1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl
5
6 Borel (measurable) space -- the smallest σ-algebra generated by open sets
7
8 It would be nice to encode this in the topological space type class, i.e. each topological space
9 carries a measurable space, the Borel space. This would be similar how each uniform space carries a
10 topological space. The idea is to allow definitional equality for product instances.
11 We would like to have definitional equality for
12
13 borel t₁ × borel t₂ = borel (t₁ × t₂)
14
15 Unfortunately, this only holds if t₁ and t₂ are second-countable topologies.
16 -/
17 import measure_theory.measurable_space topology.instances.ennreal analysis.normed_space.basic
src └─────────────────────────────┘ └────────────────────────┘ └─────────────────────────┘
18 noncomputable theory
19
20 open classical set lattice real
21 open_locale classical
22
23 universes u v w x y
24 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort y} {s t u : set α}
id └─┘
src └─┘
typ └─┘
25
26 open measurable_space topological_space
27
28 @[instance, priority 900] def borel (α : Type u) [topological_space α] : measurable_space α :=
id └───────────────┘ ┴ └──────────────┘ ┴
src └───────────────┘ └──────────────┘
typ └───────────────┘ ┴ └──────────────┘ ┴
doc └───────────────┘
29 generate_from {s : set α | is_open s}
id └───────────┘ ┴ └─┘ ┴ └─────┘ ┴
src └───────────┘ ┴ └─┘ └─────┘
typ └───────────┘ ┴ └─┘ ┴ └─────┘ ┴
doc └───────────┘ └─────┘
30
31 lemma borel_eq_generate_from_of_subbasis {s : set (set α)}
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
32 [t : topological_space α] [second_countable_topology α] (hs : t = generate_from s) :
id └───────────────┘ ┴ └───────────────────────┘ ┴ ┴ ┴ └───────────┘ ┴
src └───────────────┘ └───────────────────────┘ ┴ └───────────┘
typ └───────────────┘ ┴ └───────────────────────┘ ┴ ┴ ┴ └───────────┘ ┴
doc └───────────────┘ └───────────────────────┘ └───────────┘
33 borel α = generate_from s :=
id └───┘ ┴ ┴ └───────────┘ ┴
src └───┘ ┴ └───────────┘
typ └───┘ ┴ ┴ └───────────┘ ┴
doc └───────────┘
34 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
35 (generate_from_le $ assume u (hu : t.is_open u),
id └──────────────┘ ┴ ┴└──────┘ ┴
src └──────────────┘ └──────┘
typ └──────────────┘ ┴ ┴└──────┘ ┴
36 begin
st └─────
37 rw [hs] at hu,
id └┘
src └──┘ └─────┘
typ └──┘└┘└─────┘
doc └──┘ └─────┘
txt └──┘ └─────┘
par └──┘ └─────┘
pid └┘ ┴└────┘
st ───────────┘┴└────┘└─
38 induction hu,
id └┘
src └────────┘
typ └────────┘└┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ─────────────────┘└─
39 case generate_open.basic : u hu
src └───────────────────────────────
typ └───────────────────────────────
doc └───────────────────────────────
txt └───────────────────────────────
par └───────────────────────────────
pid └──────────────────┘└─────┘└
st ──────────────────────────────────────
40 { exact generate_measurable.basic u hu },
id └───────────────────────┘ ┴ └┘
src ───────┘└────┘└───────────────────────┘┴ ┴ ┴┴
typ ───────┘└────┘└───────────────────────┘┴┴┴└┘┴┴
doc ───────┘└────┘ ┴ ┴ ┴┴
txt ───────┘└────┘ ┴ ┴ ┴┴
par ───────┘└────┘ ┴ ┴ ┴┴
pid ─────────────┘ ┴ ┴ └┘
st ──────┘└────────────────────────────────────┘└┘└
41 case generate_open.univ
src └───────────────────────
typ └───────────────────────
doc └───────────────────────
txt └───────────────────────
par └───────────────────────
pid └─────────────────┘└
st ──────────────────────────────
42 { exact @is_measurable.univ α (generate_from s) },
id └────────────────┘ ┴ └───────────┘ ┴
src ───────┘└────┘ └────────────────┘┴ ┴ └───────────┘┴ └┘┴
typ ───────┘└────┘ └────────────────┘┴┴┴ └───────────┘┴┴└┘┴
doc ───────┘└────┘ ┴ ┴ └───────────┘┴ └┘┴
txt ───────┘└────┘ ┴ ┴ ┴ └┘┴
par ───────┘└────┘ ┴ ┴ ┴ └┘┴
pid ─────┘└──────┘ ┴ ┴ ┴ └─┘
st ──────┘└─────────────────────────────────────────────┘└┘└
43 case generate_open.inter : s₁ s₂ _ _ hs₁ hs₂
src └────────────────────────────────────────────
typ └────────────────────────────────────────────
doc └────────────────────────────────────────────
txt └────────────────────────────────────────────
par └────────────────────────────────────────────
pid └──────────────────┘└──────────────────┘└
st ───────────────────────────────────────────────────
44 { exact @is_measurable.inter α (generate_from s) _ _ hs₁ hs₂ },
id └─────────────────┘ ┴ └───────────┘ ┴ └─┘ └─┘
src ───────┘└────┘ └─────────────────┘┴ ┴ └───────────┘┴ └────┘ ┴ ┴┴
typ ───────┘└────┘ └─────────────────┘┴┴┴ └───────────┘┴┴└────┘└─┘┴└─┘┴┴
doc ───────┘└────┘ ┴ ┴ └───────────┘┴ └────┘ ┴ ┴┴
txt ───────┘└────┘ ┴ ┴ ┴ └────┘ ┴ ┴┴
par ───────┘└────┘ ┴ ┴ ┴ └────┘ ┴ ┴┴
pid ─────────────┘ ┴ ┴ ┴ └────┘ ┴ └┘
st ──────┘└──────────────────────────────────────────────────────────┘└┘└
45 case generate_open.sUnion : f hf ih {
src └─────────────────────────────────────
typ └─────────────────────────────────────
doc └─────────────────────────────────────
txt └─────────────────────────────────────
par └─────────────────────────────────────
pid └───────────────────┘└────────┘└──
st ──────────────────────────────────────────┘└
46 rcases is_open_sUnion_countable f (by rwa hs) with ⟨v, hv, vf, vu⟩,
id └──────────────────────┘ ┴ └┘
src ───────┘└─────┘└──────────────────────┘┴ ┴ ┴└──┘ └────────────────────┘└─
typ ───────┘└─────┘└──────────────────────┘┴┴┴ ┴└──┘└┘└────────────────────┘└─
doc ───────┘└─────┘ ┴ ┴ ┴└──┘ └────────────────────┘└─
txt ───────┘└─────┘ ┴ ┴ ┴└──┘ └────────────────────┘└─
par ───────┘└─────┘ ┴ ┴ ┴└──┘ └────────────────────┘└─
pid ──────────────┘ ┴ ┴ └───┘ └───────────────────────
st ────────────────────────────────────────────┘└─────┘└────────────────────┘└─
47 rw ← vu,
id └┘
src ───────┘└───┘ └─
typ ───────┘└───┘└┘└─
doc ───────┘└───┘ └─
txt ───────┘└───┘ └─
par ───────┘└───┘ └─
pid ────────────┘ └─
st ──────────────┘└─
48 exact @is_measurable.sUnion α (generate_from s) _ hv
id └──────────────────┘ ┴ └───────────┘ ┴ └┘
src ───────┘└────┘ └──────────────────┘┴ ┴ └───────────┘┴ └──┘ └
typ ───────┘└────┘ └──────────────────┘┴┴┴ └───────────┘┴┴└──┘└┘└
doc ───────┘└────┘ ┴ ┴ └───────────┘┴ └──┘ └
txt ───────┘└────┘ ┴ ┴ ┴ └──┘ └
par ───────┘└────┘ ┴ ┴ ┴ └──┘ └
pid ─────────────┘ ┴ ┴ ┴ └──┘ └
st ─────────────────────────────────────────────────────────────
49 (λ x xv, ih _ (vf xv)) }
id └┘ └┘
src ─────────┘ └─────┘ └─┘ ┴ └─┘└─
typ ─────────┘ └─────┘└┘└─┘ └┘┴ └─┘└─
doc ─────────┘ └─────┘ └─┘ ┴ └─┘└─
txt ─────────┘ └─────┘ └─┘ ┴ └─┘└─
par ─────────┘ └─────┘ └─┘ ┴ └─┘└─
pid ─────────┘ └─────┘ └─┘ ┴ └──┘└
st ────────────────────────────────┘┴└
50 end)
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
51 (generate_from_le $ assume u hu, generate_measurable.basic _ $
id └──────────────┘ ┴ └┘ └───────────────────────┘
src └──────────────┘ └───────────────────────┘
typ └──────────────┘ ┴ └┘ └───────────────────────┘
52 show t.is_open u, by rw [hs]; exact generate_open.basic _ hu)
id ┴└──────┘ ┴ └┘ └─────────────────┘ └┘
src └──────┘ └──┘ ┴ └────┘└─────────────────┘└─┘
typ ┴└──────┘ ┴ └──┘└┘┴ └────┘└─────────────────┘└─┘└┘
doc └──┘ ┴ └────┘ └─┘
txt └──┘ ┴ └────┘ └─┘
par └──┘ ┴ └────┘ └─┘
pid └┘ ┴ ┴ └─┘
st └─────┘┴└──────────────────────────────┘
53
54 lemma borel_eq_generate_Iio (α)
55 [topological_space α] [second_countable_topology α]
id └───────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────────┘
56 [linear_order α] [order_topology α] :
id └──────────┘ ┴ └────────────┘ ┴
src └──────────┘ └────────────┘
typ └──────────┘ ┴ └────────────┘ ┴
doc └────────────┘
57 borel α = generate_from (range Iio) :=
id └───┘ ┴ ┴ └───────────┘ └───┘ └─┘
src └───┘ ┴ └───────────┘ └───┘ └─┘
typ └───┘ ┴ ┴ └───────────┘ └───┘ └─┘
doc └───────────┘ └───┘ └─┘
58 begin
st └─────
59 refine le_antisymm _ (generate_from_le _),
id └─────────┘ └──────────────┘
src └─────┘└─────────┘└─┘ └──────────────┘└─┘
typ └─────┘└─────────┘└─┘ └──────────────┘└─┘
doc └─────┘ └─┘ └─┘
txt └─────┘ └─┘ └─┘
par └─────┘ └─┘ └─┘
pid ┴ └─┘ └─┘
st ──────────────────────────────────────────┘└─
60 { rw borel_eq_generate_from_of_subbasis (order_topology.topology_eq_generate_intervals α),
id └────────────────────────────────┘ └───────────────────────────────────────────┘ ┴
src └─┘└────────────────────────────────┘┴ └───────────────────────────────────────────┘┴ ┴
typ └─┘└────────────────────────────────┘┴ └───────────────────────────────────────────┘┴┴┴
doc └─┘ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───┘└─────────────────────────────────────────────────────────────────────────────────────┘└─
61 have H : ∀ a:α, is_measurable (measurable_space.generate_from (range Iio)) (Iio a) :=
id ┴ └───────────┘ └────────────────────────────┘ └───┘ └─┘
src └───────┘ └─┘ ┴└───────────┘┴ └────────────────────────────┘┴ └───┘┴ └─┘ └─┘┴ └────
typ └───────┘ └─┘┴ ┴└───────────┘┴ └────────────────────────────┘┴ └───┘┴ └─┘ └─┘┴ └────
doc └───────┘ └─┘ ┴ ┴ └────────────────────────────┘┴ └───┘┴ └─┘ └─┘┴ └────
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
par └───────┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
pid └────┘└─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└───
st ──────────────────────────────────────────────────────────────────────────────────────────
62 λ a, generate_measurable.basic _ ⟨_, rfl⟩,
id └───────────────────────┘ └─┘
src ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘┴
typ ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘┴
doc ─────┘ └──┘ └─┘ └─┘ ┴
txt ─────┘ └──┘ └─┘ └─┘ ┴
par ─────┘ └──┘ └─┘ └─┘ ┴
pid ─────┘ └──┘ └─┘ └─┘ ┴
st ──────────────────────────────────────────────┘└─
63 refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩; [skip, apply H],
id └──────────────┘ ┴
src └─────┘└──────────────┘└┘ └─────────────────────┘ ┴└──┘ └────┘
typ └─────┘└──────────────┘└┘ └─────────────────────┘ ┴└──┘ └────┘
doc └─────┘ └┘ └─────────────────────┘ └──┘ └────┘
txt └─────┘ └┘ └─────────────────────┘ └──┘ └────┘
par └─────┘ └┘ └─────────────────────┘ └──┘ └────┘
pid ┴ └┘ └───────────────┘ ┴
st ────────────────────────────┘└────────────────────────────────────────┘└─
64 by_cases h : ∃ a', ∀ b, a < b ↔ a' ≤ b,
id ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘┴└─┘┴┴ └┘ ┴ ┴┴┴ ┴┴┴ ┴┴┴
typ └───────┘ └─┘┴└─┘┴┴ └┘ ┴┴┴┴┴ ┴┴┴ ┴┴┴
doc └───────┘ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
65 { rcases h with ⟨a', ha'⟩,
id ┴
src └─────┘ └─────────────┘
typ └─────┘┴└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ─────┘└─────────────────────┘└─
66 rw (_ : Ioi a = -Iio a'), {exact (H _).compl _},
id └─┘ ┴ ┴ ┴└─┘ └┘ ┴
src └─┘ └──┘└─┘┴ ┴┴┴┴└─┘┴ ┴ └────┘ └─────────┘
typ └─┘ └──┘└─┘┴┴┴┴┴┴└─┘┴└┘┴ └────┘ ┴└─────────┘
doc └─┘ └──┘└─┘┴ ┴ ┴ └─┘┴ ┴ └────┘ └─────────┘
txt └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─────────┘
par └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─────────┘
pid ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
st ─────────────────────────────┘└────────────────────┘└┘└
67 simp [set.ext_iff, ha'] },
id └─────────┘ └─┘
src └────┘└─────────┘└┘ └┘
typ └────┘└─────────┘└┘└─┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────────┘└┘└
68 { rcases is_open_Union_countable
id └─────────────────────┘
src └─────┘└─────────────────────┘└
typ └─────┘└─────────────────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────────────────────
69 (λ a' : {a' : α // a < a'}, {b | a'.1 < b})
id ┴ ┴ ┴ ┴
src ───────┘ └────┘┴└───┘ └──┘ ┴ ┴ └─┘┴└──┘ └─┘ ┴ └──
typ ───────┘ └────┘┴└───┘┴└──┘┴┴ ┴ └─┘┴└──┘ └─┘ ┴ └──
doc ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ └─┘ ┴ └──
txt ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ └─┘ ┴ └──
par ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ └─┘ ┴ └──
pid ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ └─┘ ┴ └──
st ────────────────────────────────────────────────────
70 (λ a', is_open_lt' _) with ⟨v, ⟨hv⟩, vu⟩,
id └─────────┘
src ───────┘ └───┘└─────────┘└────────────────────┘
typ ───────┘ └───┘└─────────┘└────────────────────┘
doc ───────┘ └───┘ └────────────────────┘
txt ───────┘ └───┘ └────────────────────┘
par ───────┘ └───┘ └────────────────────┘
pid ───────┘ └───┘ └────────────────────┘
st ───────────────────────────────────────────────┘└─
71 simp [set.ext_iff] at vu,
id └─────────┘
src └────┘└─────────┘└─────┘
typ └────┘└─────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ─────────────────────────────┘└─
72 have : Ioi a = ⋃ x : v, -Iio x.1.1,
id └─┘ ┴ ┴ ┴┴ └─┘
src └─────┘└─┘┴ ┴ ┴┴└───┘ ┴┴ └─┘┴ └──┘
typ └─────┘└─┘┴┴┴ ┴┴└───┘┴┴┴ └─┘┴ └──┘
doc └─────┘└─┘┴ ┴ ┴┴└───┘ ┴┴ └─┘┴ └──┘
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘└┘
st ───────────────────────────────────────┘└─
73 { simp [set.ext_iff],
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───────┘└────────────────┘└─
74 refine λ x, ⟨λ ax, _, λ ⟨a', ⟨h, av⟩, ax⟩, lt_of_lt_of_le h ax⟩,
id ┴ └┘ └────────────┘
src └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘└────────────┘┴ ┴ ┴
typ └─────┘ └──┘ └──────┘ └┘ └┘ ┴└┘ └─┘└┘└─┘└────────────┘┴ ┴ ┴
doc └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
txt └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
par └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
pid ┴ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
75 rcases (vu x).2 _ with ⟨a', h₁, h₂⟩,
id └┘ ┴
src └─────┘ ┴ └─────────────────────┘
typ └─────┘ └┘┴┴└─────────────────────┘
doc └─────┘ ┴ └─────────────────────┘
txt └─────┘ ┴ └─────────────────────┘
par └─────┘ ┴ └─────────────────────┘
pid ┴ ┴ └─────────────────────┘
st ──────────────────────────────────────────┘└─
76 { exact ⟨a', h₁, le_of_lt h₂⟩ },
id └┘ └┘ └──────┘ └┘
src └────┘ └┘ └┘└──────┘┴ └┘
typ └────┘ └┘└┘└┘└┘└──────┘┴└┘└┘
doc └────┘ └┘ └┘ ┴ └┘
txt └────┘ └┘ └┘ ┴ └┘
par └────┘ └┘ └┘ ┴ └┘
pid ┴ └┘ └┘ ┴ ┴┴
st ─────────┘└──────────────────────────┘└┘└
77 refine not_imp_comm.1 (λ h, _) h,
id └──────────┘ ┴
src └─────┘└──────────┘└─┘ └─────┘
typ └─────┘└──────────┘└─┘ └─────┘┴
doc └─────┘ └─┘ └─────┘
txt └─────┘ └─┘ └─────┘
par └─────┘ └─┘ └─────┘
pid ┴ └─┘ └─────┘
st ───────────────────────────────────────┘└─
78 exact ⟨x, λ b, ⟨λ ab, le_of_not_lt (λ h', h ⟨b, ab, h'⟩),
id ┴ └──────────┘ ┴
src └────┘ └┘ └──┘ └───┘└──────────┘┴ └───┘ ┴ └┘ └┘ └───
typ └────┘ ┴└┘ └──┘ └───┘└──────────┘┴ └───┘┴┴ └┘ └┘ └───
doc └────┘ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
txt └────┘ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
par └────┘ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
pid ┴ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
st ──────────────────────────────────────────────────────────────────
79 lt_of_lt_of_le ax⟩⟩ },
id └────────────┘ └┘
src ─────────┘└────────────┘┴ └─┘
typ ─────────┘└────────────┘┴└┘└─┘
doc ─────────┘ ┴ └─┘
txt ─────────┘ ┴ └─┘
par ─────────┘ ┴ └─┘
pid ─────────┘ ┴ └┘┴
st ─────────────────────────────┘└┘└
80 rw this, resetI,
id └──┘
src └─┘ └────┘
typ └─┘└──┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴
st ────────────┘└─────────
81 apply is_measurable.Union,
id └─────────────────┘
src └────┘└─────────────────┘
typ └────┘└─────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
82 exact λ _, (H _).compl _ } },
id ┴
src └────┘ └──┘ └──────────┘
typ └────┘ └──┘ ┴└──────────┘
doc └────┘ └──┘ └──────────┘
txt └────┘ └──┘ └──────────┘
par └────┘ └──┘ └──────────┘
pid ┴ └──┘ └─────────┘┴
st ──────────────────────────────┘└──┘└
83 { simp, rintro _ a rfl,
src └──┘ └────────────┘
typ └──┘ └────────────┘
doc └──┘ └────────────┘
txt └──┘ └────────────┘
par └──┘ └────────────┘
pid └──────┘
st ───────┘└──────────────┘└─
84 exact generate_measurable.basic _ is_open_Iio }
id └───────────────────────┘ └─────────┘
src └────┘└───────────────────────┘└─┘└─────────┘┴
typ └────┘└───────────────────────┘└─┘└─────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────────────────────────────┘└─
85 end
st ──┘
86
87 lemma borel_eq_generate_Ioi (α)
88 [topological_space α] [second_countable_topology α]
id └───────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────────┘
89 [linear_order α] [order_topology α] :
id └──────────┘ ┴ └────────────┘ ┴
src └──────────┘ └────────────┘
typ └──────────┘ ┴ └────────────┘ ┴
doc └────────────┘
90 borel α = generate_from (range (λ a, {x | a < x})) :=
id └───┘ ┴ ┴ └───────────┘ └───┘ ┴ ┴┴ ┴ ┴ ┴
src └───┘ ┴ └───────────┘ └───┘ ┴ ┴
typ └───┘ ┴ ┴ └───────────┘ └───┘ ┴ ┴┴ ┴ ┴ ┴
doc └───────────┘ └───┘
91 begin
st └─────
92 refine le_antisymm _ (generate_from_le _),
id └─────────┘ └──────────────┘
src └─────┘└─────────┘└─┘ └──────────────┘└─┘
typ └─────┘└─────────┘└─┘ └──────────────┘└─┘
doc └─────┘ └─┘ └─┘
txt └─────┘ └─┘ └─┘
par └─────┘ └─┘ └─┘
pid ┴ └─┘ └─┘
st ──────────────────────────────────────────┘└─
93 { rw borel_eq_generate_from_of_subbasis (order_topology.topology_eq_generate_intervals α),
id └────────────────────────────────┘ └───────────────────────────────────────────┘ ┴
src └─┘└────────────────────────────────┘┴ └───────────────────────────────────────────┘┴ ┴
typ └─┘└────────────────────────────────┘┴ └───────────────────────────────────────────┘┴┴┴
doc └─┘ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───┘└─────────────────────────────────────────────────────────────────────────────────────┘└─
94 have H : ∀ a:α, is_measurable (measurable_space.generate_from (range (λ a, {x | a < x}))) {x | a < x} :=
id ┴ └───────────┘ └────────────────────────────┘ └───┘ ┴ ┴
src └───────┘ └─┘ ┴└───────────┘┴ └────────────────────────────┘┴ └───┘┴ └──┘ └──┘ ┴┴┴ └───┘┴└──┘ ┴ ┴ └────
typ └───────┘ └─┘┴ ┴└───────────┘┴ └────────────────────────────┘┴ └───┘┴ └──┘ └──┘ ┴┴┴ └───┘┴└──┘ ┴ ┴ └────
doc └───────┘ └─┘ ┴ ┴ └────────────────────────────┘┴ └───┘┴ └──┘ └──┘ ┴ ┴ └───┘ └──┘ ┴ ┴ └────
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └───┘ └──┘ ┴ ┴ └────
par └───────┘ └─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └───┘ └──┘ ┴ ┴ └────
pid └────┘└─┘ └─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └───┘ └──┘ ┴ ┴ ┴└───
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
95 λ a, generate_measurable.basic _ ⟨_, rfl⟩,
id └───────────────────────┘ └─┘
src ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘┴
typ ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘┴
doc ─────┘ └──┘ └─┘ └─┘ ┴
txt ─────┘ └──┘ └─┘ └─┘ ┴
par ─────┘ └──┘ └─┘ └─┘ ┴
pid ─────┘ └──┘ └─┘ └─┘ ┴
st ──────────────────────────────────────────────┘└─
96 refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩, {apply H},
id └──────────────┘
src └─────┘└──────────────┘└┘ └─────────────────────┘ └────┘
typ └─────┘└──────────────┘└┘ └─────────────────────┘ └────┘
doc └─────┘ └┘ └─────────────────────┘ └────┘
txt └─────┘ └┘ └─────────────────────┘ └────┘
par └─────┘ └┘ └─────────────────────┘ └────┘
pid ┴ └┘ └───────────────┘ ┴
st ────────────────────────────┘└───────────────────────┘└────────┘└┘└
97 by_cases h : ∃ a', ∀ b, b < a ↔ b ≤ a',
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘┴└─┘┴┴ └┘ ┴ ┴ ┴ ┴┴┴ ┴┴┴
typ └───────┘ └─┘┴└─┘┴┴ └┘ ┴ ┴ ┴┴┴┴┴ ┴┴┴
doc └───────┘ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
98 { rcases h with ⟨a', ha'⟩,
id ┴
src └─────┘ └─────────────┘
typ └─────┘┴└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ─────┘└─────────────────────┘└─
99 rw (_ : Iio a = -Ioi a'), {exact (H _).compl _},
id └─┘ ┴ ┴ ┴└─┘ └┘ ┴
src └─┘ └──┘└─┘┴ ┴┴┴┴└─┘┴ ┴ └────┘ └─────────┘
typ └─┘ └──┘└─┘┴┴┴┴┴┴└─┘┴└┘┴ └────┘ ┴└─────────┘
doc └─┘ └──┘└─┘┴ ┴ ┴ └─┘┴ ┴ └────┘ └─────────┘
txt └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─────────┘
par └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─────────┘
pid ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
st ─────────────────────────────┘└────────────────────┘└┘└
100 simp [set.ext_iff, ha'] },
id └─────────┘ └─┘
src └────┘└─────────┘└┘ └┘
typ └────┘└─────────┘└┘└─┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────────┘└┘└
101 { rcases is_open_Union_countable
id └─────────────────────┘
src └─────┘└─────────────────────┘└
typ └─────┘└─────────────────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────────────────────
102 (λ a' : {a' : α // a' < a}, {b | b < a'.1})
id ┴ ┴ ┴ ┴
src ───────┘ └────┘┴└───┘ └──┘ ┴ ┴ └─┘┴└──┘ ┴ ┴ └────
typ ───────┘ └────┘┴└───┘┴└──┘ ┴ ┴┴└─┘┴└──┘ ┴ ┴ └────
doc ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ ┴ ┴ └────
txt ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ ┴ ┴ └────
par ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ ┴ ┴ └────
pid ───────┘ └────┘ └───┘ └──┘ ┴ ┴ └─┘ └──┘ ┴ ┴ └────
st ────────────────────────────────────────────────────
103 (λ a', is_open_gt' _) with ⟨v, ⟨hv⟩, vu⟩,
id └─────────┘
src ───────┘ └───┘└─────────┘└────────────────────┘
typ ───────┘ └───┘└─────────┘└────────────────────┘
doc ───────┘ └───┘ └────────────────────┘
txt ───────┘ └───┘ └────────────────────┘
par ───────┘ └───┘ └────────────────────┘
pid ───────┘ └───┘ └────────────────────┘
st ───────────────────────────────────────────────┘└─
104 simp [set.ext_iff] at vu,
id └─────────┘
src └────┘└─────────┘└─────┘
typ └────┘└─────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ─────────────────────────────┘┴┴
105 have : Iio a = ⋃ x : v, -Ioi x.1.1,
id └─┘ ┴ ┴ ┴┴ └─┘
src └─────┘└─┘┴ ┴ ┴┴└───┘ ┴┴ └─┘┴ └──┘
typ └─────┘└─┘┴┴┴ ┴┴└───┘┴┴┴ └─┘┴ └──┘
doc └─────┘└─┘┴ ┴ ┴┴└───┘ ┴┴ └─┘┴ └──┘
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘└┘
st └──────────────────────────────────────┘└─
106 { simp [set.ext_iff],
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───────┘└────────────────┘└─
107 refine λ x, ⟨λ ax, _, λ ⟨a', ⟨h, av⟩, ax⟩, lt_of_le_of_lt ax h⟩,
id ┴ └┘ └────────────┘
src └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘└────────────┘┴ ┴ ┴
typ └─────┘ └──┘ └──────┘ └┘ └┘ ┴└┘ └─┘└┘└─┘└────────────┘┴ ┴ ┴
doc └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
txt └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
par └─────┘ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
pid ┴ └──┘ └──────┘ └┘ └┘ └┘ └─┘ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
108 rcases (vu x).2 _ with ⟨a', h₁, h₂⟩,
id └┘ ┴
src └─────┘ ┴ └─────────────────────┘
typ └─────┘ └┘┴┴└─────────────────────┘
doc └─────┘ ┴ └─────────────────────┘
txt └─────┘ ┴ └─────────────────────┘
par └─────┘ ┴ └─────────────────────┘
pid ┴ ┴ └─────────────────────┘
st ──────────────────────────────────────────┘└─
109 { exact ⟨a', h₁, le_of_lt h₂⟩ },
id └┘ └┘ └──────┘ └┘
src └────┘ └┘ └┘└──────┘┴ └┘
typ └────┘ └┘└┘└┘└┘└──────┘┴└┘└┘
doc └────┘ └┘ └┘ ┴ └┘
txt └────┘ └┘ └┘ ┴ └┘
par └────┘ └┘ └┘ ┴ └┘
pid ┴ └┘ └┘ ┴ ┴┴
st ─────────┘└──────────────────────────┘└┘└
110 refine not_imp_comm.1 (λ h, _) h,
id └──────────┘ ┴
src └─────┘└──────────┘└─┘ └─────┘
typ └─────┘└──────────┘└─┘ └─────┘┴
doc └─────┘ └─┘ └─────┘
txt └─────┘ └─┘ └─────┘
par └─────┘ └─┘ └─────┘
pid ┴ └─┘ └─────┘
st ───────────────────────────────────────┘└─
111 exact ⟨x, λ b, ⟨λ ab, le_of_not_lt (λ h', h ⟨b, ab, h'⟩),
id ┴ └──────────┘ ┴
src └────┘ └┘ └──┘ └───┘└──────────┘┴ └───┘ ┴ └┘ └┘ └───
typ └────┘ ┴└┘ └──┘ └───┘└──────────┘┴ └───┘┴┴ └┘ └┘ └───
doc └────┘ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
txt └────┘ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
par └────┘ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
pid ┴ └┘ └──┘ └───┘ ┴ └───┘ ┴ └┘ └┘ └───
st ──────────────────────────────────────────────────────────────────
112 λ h, lt_of_le_of_lt h ax⟩⟩ },
id └────────────┘ └┘
src ─────────┘ └──┘└────────────┘┴ ┴ └─┘
typ ─────────┘ └──┘└────────────┘┴ ┴└┘└─┘
doc ─────────┘ └──┘ ┴ ┴ └─┘
txt ─────────┘ └──┘ ┴ ┴ └─┘
par ─────────┘ └──┘ ┴ ┴ └─┘
pid ─────────┘ └──┘ ┴ ┴ └┘┴
st ────────────────────────────────────┘└┘└
113 rw this, resetI,
id └──┘
src └─┘ └────┘
typ └─┘└──┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴
st ────────────┘└─────────
114 apply is_measurable.Union,
id └─────────────────┘
src └────┘└─────────────────┘
typ └────┘└─────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
115 exact λ _, (H _).compl _ } },
id ┴
src └────┘ └──┘ └──────────┘
typ └────┘ └──┘ ┴└──────────┘
doc └────┘ └──┘ └──────────┘
txt └────┘ └──┘ └──────────┘
par └────┘ └──┘ └──────────┘
pid ┴ └──┘ └─────────┘┴
st ──────────────────────────────┘└──┘└
116 { simp, rintro _ a rfl,
src └──┘ └────────────┘
typ └──┘ └────────────┘
doc └──┘ └────────────┘
txt └──┘ └────────────┘
par └──┘ └────────────┘
pid └──────┘
st ───────┘└──────────────┘└─
117 exact generate_measurable.basic _ (is_open_lt' _) }
id └───────────────────────┘ └─────────┘
src └────┘└───────────────────────┘└─┘ └─────────┘└──┘
typ └────┘└───────────────────────┘└─┘ └─────────┘└──┘
doc └────┘ └─┘ └──┘
txt └────┘ └─┘ └──┘
par └────┘ └─┘ └──┘
pid ┴ └─┘ └─┘┴
st ─────────────────────────────────────────────────────┘└─
118 end
st ──┘
119
120 lemma borel_comap {f : α → β} {t : topological_space β} :
id ┴ ┴ └───────────────┘ ┴
src └───────────────┘
typ ┴ ┴ └───────────────┘ ┴
doc └───────────────┘
121 @borel α (t.induced f) = (@borel β t).comap f :=
id └───┘ ┴ ┴└──────┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
src └───┘ └──────┘ ┴ └───┘ └───┘
typ └───┘ ┴ ┴└──────┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
doc └──────┘ └───┘
122 calc @borel α (t.induced f) =
id └───┘ ┴ ┴└──────┘ ┴
src └───┘ └──────┘
typ └───┘ ┴ ┴└──────┘ ┴
doc └──────┘
123 measurable_space.generate_from (preimage f '' {s | is_open s }) :
id └────────────────────────────┘ └──────┘ ┴ └┘ ┴┴ └─────┘ ┴
src └────────────────────────────┘ └──────┘ └┘ ┴ └─────┘
typ └────────────────────────────┘ └──────┘ ┴ └┘ ┴┴ └─────┘ ┴
doc └────────────────────────────┘ └──────┘ └─────┘
124 congr_arg measurable_space.generate_from $ set.ext $ assume s : set α,
id └───────┘ └────────────────────────────┘ └─────┘ └─┘ ┴
src └───────┘ └────────────────────────────┘ └─────┘ └─┘
typ └───────┘ └────────────────────────────┘ └─────┘ └─┘ ┴
doc └────────────────────────────┘
125 show (t.induced f).is_open s ↔ s ∈ preimage f '' {s | is_open s},
id ┴└──────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴┴ └─────┘ ┴
src └──────┘ └─────┘ ┴ ┴ └──────┘ └┘ ┴ └─────┘
typ ┴└──────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴┴ └─────┘ ┴
doc └──────┘ └──────┘ └─────┘
126 by simp [topological_space.induced, set.image, eq_comm]; refl
id └───────────────────────┘ └───────┘ └─────┘
src └────┘└───────────────────────┘└┘└───────┘└┘└─────┘┴ └────
typ └────┘└───────────────────────┘└┘└───────┘└┘└─────┘┴ └────
doc └────┘└───────────────────────┘└┘ └┘ ┴ └────
txt └────┘ └┘ └┘ ┴ └────
par └────┘ └┘ └┘ ┴ └────
pid ┴┴ └┘ └┘ ┴ └
st └───────────────────────────────────────────────────────────
127 ... = (@borel β t).comap f : comap_generate_from.symm
id └───┘ ┴ ┴ └───┘ ┴ └─────────────────┘└───┘
src ─┘ └───┘ └───┘ └─────────────────┘└───┘
typ ─┘ └───┘ ┴ ┴ └───┘ ┴ └─────────────────┘└───┘
doc ─┘ └───┘
txt ─┘
par ─┘
pid ─┘
st ─┘
128
129 section
130 variables [topological_space α]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
131
132 lemma is_measurable_of_is_open : is_open s → is_measurable s := generate_measurable.basic s
id └─────┘ ┴ └───────────┘ ┴ └───────────────────────┘ ┴
src └─────┘ └───────────┘ └───────────────────────┘
typ └─────┘ ┴ └───────────┘ ┴ └───────────────────────┘ ┴
doc └─────┘ └───────────┘
133
134 lemma is_measurable_interior : is_measurable (interior s) :=
id └───────────┘ └──────┘ ┴
src └───────────┘ └──────┘
typ └───────────┘ └──────┘ ┴
doc └───────────┘ └──────┘
135 is_measurable_of_is_open is_open_interior
id └──────────────────────┘ └──────────────┘
src └──────────────────────┘ └──────────────┘
typ └──────────────────────┘ └──────────────┘
136
137 lemma is_measurable_ball [metric_space β] {x : β} {ε : ℝ} : is_measurable (metric.ball x ε) :=
id └──────────┘ ┴ ┴ ┴ └───────────┘ └─────────┘ ┴ ┴
src └──────────┘ ┴ └───────────┘ └─────────┘
typ └──────────┘ ┴ ┴ ┴ └───────────┘ └─────────┘ ┴ ┴
doc └──────────┘ └───────────┘ └─────────┘
138 is_measurable_of_is_open metric.is_open_ball
id └──────────────────────┘ └─────────────────┘
src └──────────────────────┘ └─────────────────┘
typ └──────────────────────┘ └─────────────────┘
139
140 lemma is_measurable_of_is_closed (h : is_closed s) : is_measurable s :=
id └───────┘ ┴ └───────────┘ ┴
src └───────┘ └───────────┘
typ └───────┘ ┴ └───────────┘ ┴
doc └───────┘ └───────────┘
141 is_measurable.compl_iff.1 $ is_measurable_of_is_open h
id └─────────────────────┘┴ └──────────────────────┘ ┴
src └─────────────────────┘┴ └──────────────────────┘
typ └─────────────────────┘┴ └──────────────────────┘ ┴
142
143 lemma is_measurable_singleton [t1_space α] {x : α} : is_measurable ({x} : set α) :=
id └──────┘ ┴ ┴ └───────────┘ ┴┴ └─┘ ┴
src └──────┘ └───────────┘ ┴ └─┘
typ └──────┘ ┴ ┴ └───────────┘ ┴┴ └─┘ ┴
doc └──────┘ └───────────┘
144 is_measurable_of_is_closed is_closed_singleton
id └────────────────────────┘ └─────────────────┘
src └────────────────────────┘ └─────────────────┘
typ └────────────────────────┘ └─────────────────┘
145
146 lemma is_measurable_closure : is_measurable (closure s) :=
id └───────────┘ └─────┘ ┴
src └───────────┘ └─────┘
typ └───────────┘ └─────┘ ┴
doc └───────────┘ └─────┘
147 is_measurable_of_is_closed is_closed_closure
id └────────────────────────┘ └───────────────┘
src └────────────────────────┘ └───────────────┘
typ └────────────────────────┘ └───────────────┘
148
149 lemma measurable_of_continuous [topological_space β] {f : α → β} (h : continuous f) :
id └───────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └───────────────┘ └────────┘
typ └───────────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └───────────────┘ └────────┘
150 measurable f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
151 measurable_generate_from $ assume t ht, is_measurable_of_is_open $ h t ht
id └──────────────────────┘ ┴ └┘ └──────────────────────┘ ┴ ┴ └┘
src └──────────────────────┘ └──────────────────────┘
typ └──────────────────────┘ ┴ └┘ └──────────────────────┘ ┴ ┴ └┘
152
153 lemma borel_prod_le [topological_space β] :
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
154 prod.measurable_space ≤ borel (α × β) :=
id └───────────────────┘ ┴ └───┘ ┴ ┴ ┴
src └───────────────────┘ ┴ └───┘ ┴
typ └───────────────────┘ ┴ └───┘ ┴ ┴ ┴
155 sup_le
id └────┘
src └────┘
typ └────┘
156 (comap_le_iff_le_map.mpr $ measurable_of_continuous continuous_fst)
id └─────────────────┘└──┘ └──────────────────────┘ └────────────┘
src └─────────────────┘└──┘ └──────────────────────┘ └────────────┘
typ └─────────────────┘└──┘ └──────────────────────┘ └────────────┘
157 (comap_le_iff_le_map.mpr $ measurable_of_continuous continuous_snd)
id └─────────────────┘└──┘ └──────────────────────┘ └────────────┘
src └─────────────────┘└──┘ └──────────────────────┘ └────────────┘
typ └─────────────────┘└──┘ └──────────────────────┘ └────────────┘
158
159 lemma borel_induced {α β} [t : topological_space β] (f : α → β) :
id └───────────────┘ ┴ ┴ ┴
src └───────────────┘
typ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘
160 @borel α (t.induced f) = (borel β).comap f :=
id └───┘ ┴ ┴└──────┘ ┴ ┴ └───┘ ┴ └───┘ ┴
src └───┘ └──────┘ ┴ └───┘ └───┘
typ └───┘ ┴ ┴└──────┘ ┴ ┴ └───┘ ┴ └───┘ ┴
doc └──────┘ └───┘
161 comap_generate_from.symm
id └─────────────────┘└───┘
src └─────────────────┘└───┘
typ └─────────────────┘└───┘
162
163 lemma borel_eq_subtype (s : set α) : borel s = subtype.measurable_space :=
id └─┘ ┴ └───┘ ┴ ┴ └──────────────────────┘
src └─┘ └───┘ ┴ └──────────────────────┘
typ └─┘ ┴ └───┘ ┴ ┴ └──────────────────────┘
164 borel_induced coe
id └───────────┘ └─┘
src └───────────┘ └─┘
typ └───────────┘ └─┘
165
166 lemma borel_prod [second_countable_topology α] [topological_space β] [second_countable_topology β] :
id └───────────────────────┘ ┴ └───────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────────────┘ └───────────────┘ └───────────────────────┘
typ └───────────────────────┘ ┴ └───────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────────────┘ └───────────────┘ └───────────────────────┘
167 prod.measurable_space = borel (α × β) :=
id └───────────────────┘ ┴ └───┘ ┴ ┴ ┴
src └───────────────────┘ ┴ └───┘ ┴
typ └───────────────────┘ ┴ └───┘ ┴ ┴ ┴
168 let ⟨a, ha₁, ha₂, ha₃, ha₄, ha₅⟩ := @is_open_generated_countable_inter α _ _ in
id └─┘ └───────────────────────────────┘ ┴
src └───────────────────────────────┘
typ └─┘ └───────────────────────────────┘ ┴
169 let ⟨b, hb₁, hb₂, hb₃, hb₄, hb₅⟩ := @is_open_generated_countable_inter β _ _ in
id └─┘ └───────────────────────────────┘ ┴
src └───────────────────────────────┘
typ └─┘ └───────────────────────────────┘ ┴
170 le_antisymm borel_prod_le begin
id └─────────┘ └───────────┘
src └─────────┘ └───────────┘
typ └─────────┘ └───────────┘
st └─────
171 have : prod.topological_space = generate_from {g | ∃u∈a, ∃v∈b, g = set.prod u v},
id └────────────────────┘ ┴ └───────────┘ ┴ ┴ ┴┴ ┴ └──────┘
src └─────┘└────────────────────┘┴┴┴└───────────┘┴┴└──┘┴└┘ ┴┴ └┘ ┴ ┴ ┴└──────┘┴ ┴ ┴
typ └─────┘└────────────────────┘┴┴┴└───────────┘┴┴└──┘┴└┘┴┴┴ └┘┴ ┴ ┴ ┴└──────┘┴ ┴ ┴
doc └─────┘ ┴ ┴└───────────┘┴ └──┘ └┘ ┴ └┘ ┴ ┴ ┴└──────┘┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └──┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ └──┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ └──┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
172 { rw [ha₅, hb₅], exact prod_generate_from_generate_from_eq ha₄ hb₄ },
id └─┘ └─┘ └─────────────────────────────────┘ └─┘ └─┘
src └──┘ └┘ ┴ └────┘└─────────────────────────────────┘┴ ┴ ┴
typ └──┘└─┘└┘└─┘┴ └────┘└─────────────────────────────────┘┴└─┘┴└─┘┴
doc └──┘ └┘ ┴ └────┘ ┴ ┴ ┴
txt └──┘ └┘ ┴ └────┘ ┴ ┴ ┴
par └──┘ └┘ ┴ └────┘ ┴ ┴ ┴
pid └┘ └┘ ┴ ┴ ┴ ┴ ┴
st ─────┘└─────┘└───┘└───────────────────────────────────────────────────┘└┘└
173 rw [borel_eq_generate_from_of_subbasis this],
id └────────────────────────────────┘ └──┘
src └──┘└────────────────────────────────┘┴ ┴
typ └──┘└────────────────────────────────┘┴└──┘┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ──────────────────────────────────────────────┘└──
174 exact generate_from_le (assume p ⟨u, hu, v, hv, eq⟩,
id └──────────────┘ ┴ ┴ └┘
src └────┘└──────────────┘┴ └──┘ └┘ └┘ └┘ └┘└┘└──
typ └────┘└──────────────┘┴ └──┘┴└┘ └┘┴└┘ └┘└┘└──
doc └────┘ ┴ └──┘ └┘ └┘ └┘ └┘ └──
txt └────┘ ┴ └──┘ └┘ └┘ └┘ └┘ └──
par └────┘ ┴ └──┘ └┘ └┘ └┘ └┘ └──
pid ┴ ┴ └──┘ └┘ └┘ └┘ └┘ └──
st ─────────────────────────────────────────────────────────
175 have hu : is_open u, by rw [ha₅]; exact generate_open.basic _ hu,
id └─┘ └─────────────────┘ └┘
src ─────┘ └────┘ ┴ └───┘└──┘ ┴└──────┘└─────────────────┘└─┘ └─
typ ─────┘ └────┘ ┴ └───┘└──┘└─┘┴└──────┘└─────────────────┘└─┘└┘└─
doc ─────┘ └────┘ ┴ └───┘└──┘ ┴└──────┘ └─┘ └─
txt ─────┘ └────┘ ┴ └───┘└──┘ ┴└──────┘ └─┘ └─
par ─────┘ └────┘ ┴ └───┘└──┘ ┴└──────┘ └─┘ └─
pid ─────┘ └────┘ ┴ └───────┘ └───────┘ └─┘ └─
st ────────────────────────────┘└──────┘┴└──────────────────────────────┘└─
176 have hv : is_open v, by rw [hb₅]; exact generate_open.basic _ hv,
id └─────┘ └─┘ └─────────────────┘ └┘
src ─────┘ └────┘└─────┘┴ └───┘└──┘ ┴└──────┘└─────────────────┘└─┘ └─
typ ─────┘ └────┘└─────┘┴ └───┘└──┘└─┘┴└──────┘└─────────────────┘└─┘└┘└─
doc ─────┘ └────┘└─────┘┴ └───┘└──┘ ┴└──────┘ └─┘ └─
txt ─────┘ └────┘ ┴ └───┘└──┘ ┴└──────┘ └─┘ └─
par ─────┘ └────┘ ┴ └───┘└──┘ ┴└──────┘ └─┘ └─
pid ─────┘ └────┘ ┴ └───────┘ └───────┘ └─┘ └─
st ────────────────────────────┘└──────┘┴└──────────────────────────────┘└─
177 eq.symm ▸ is_measurable_set_prod (is_measurable_of_is_open hu) (is_measurable_of_is_open hv))
id └───┘ ┴ └────────────────────┘ └──────────────────────┘
src ─────┘ └───┘┴┴┴└────────────────────┘┴ ┴ └┘ └──────────────────────┘┴ └─┘
typ ─────┘ └───┘┴┴┴└────────────────────┘┴ ┴ └┘ └──────────────────────┘┴ └─┘
doc ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
txt ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
par ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
pid ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────────────┘
178 end
st └─┘
179
180 lemma measurable_of_continuous2 {α β γ}
181 [topological_space α] [second_countable_topology α]
id └───────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────────┘
182 [topological_space β] [second_countable_topology β]
id └───────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────────┘
183 [topological_space γ] [measurable_space δ] {f : δ → α} {g : δ → β} {c : α → β → γ}
id └───────────────┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ └──────────────┘
typ └───────────────┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘
184 (h : continuous (λp:α×β, c p.1 p.2)) (hf : measurable f) (hg : measurable g) :
id └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ ┴ ┴ ┴ └────────┘ └────────┘
typ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘ └────────┘
185 measurable (λa, c (f a) (g a)) :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
186 show measurable ((λp:α×β, c p.1 p.2) ∘ (λa, (f a, g a))),
id └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └────────┘
187 begin
st └─────
188 apply measurable.comp,
id └─────────────┘
src └────┘└─────────────┘
typ └────┘└─────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘└─
189 { rw borel_prod,
id └────────┘
src └─┘└────────┘
typ └─┘└────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└───────────┘└─
190 exact measurable_of_continuous h },
id └──────────────────────┘ ┴
src └────┘└──────────────────────┘┴ ┴
typ └────┘└──────────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────┘└┘└
191 { exact measurable.prod_mk hf hg }
id └────────────────┘ └┘ └┘
src └────┘└────────────────┘┴ ┴ ┴
typ └────┘└────────────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
192 end
st ──┘
193
194 lemma measurable.add
195 [add_monoid α] [topological_add_monoid α] [second_countable_topology α] [measurable_space β]
id └────────┘ ┴ └────────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
src └────────┘ └────────────────────┘ └───────────────────────┘ └──────────────┘
typ └────────┘ ┴ └────────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
doc └────────────────────┘ └───────────────────────┘
196 {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a + g a) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
197 measurable_of_continuous2 continuous_add
id └───────────────────────┘ └────────────┘
src └───────────────────────┘ └────────────┘
typ └───────────────────────┘ └────────────┘
198
199 lemma measurable_finset_sum {ι : Type*}
200 [add_comm_monoid α] [topological_add_monoid α] [second_countable_topology α] [measurable_space β]
id └─────────────┘ ┴ └────────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
src └─────────────┘ └────────────────────┘ └───────────────────────┘ └──────────────┘
typ └─────────────┘ ┴ └────────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
doc └────────────────────┘ └───────────────────────┘
201 {f : ι → β → α} (s : finset ι) (hf : ∀i, measurable (f i)) : measurable (λa, s.sum (λi, f i a)) :=
id ┴ ┴ ┴ └────┘ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
src └────┘ └────────┘ └────────┘ └──┘
typ ┴ ┴ ┴ └────┘ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
doc └────┘ └────────┘ └────────┘
202 finset.induction_on s
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
doc └─────────────────┘
203 (by simpa using measurable_const)
id └──────────────┘
src └──────────┘└──────────────┘
typ └──────────┘└──────────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └───────────────────────────┘
204 (assume i s his ih, by simpa [his] using measurable.add (hf i) ih)
id ┴ ┴ └─┘ └┘ └─┘ └────────────┘ └┘ ┴ └┘
src └─────┘ └──────┘└────────────┘┴ ┴ └┘
typ ┴ ┴ └─┘ └┘ └─────┘└─┘└──────┘└────────────┘┴ └┘┴┴└┘└┘
doc └─────┘ └──────┘ ┴ ┴ └┘
txt └─────┘ └──────┘ ┴ ┴ └┘
par └─────┘ └──────┘ ┴ ┴ └┘
pid ┴┴ ┴┴└────┘ ┴ ┴ └┘
st └─────────────────────────────────────────┘
205
206 lemma measurable.neg
207 [add_group α] [topological_add_group α] [measurable_space β] {f : β → α}
id └───────┘ ┴ └───────────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
src └───────┘ └───────────────────┘ └──────────────┘
typ └───────┘ ┴ └───────────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
doc └───────────────────┘
208 (hf : measurable f) : measurable (λa, - f a) :=
id └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
209 (measurable_of_continuous continuous_neg).comp hf
id └──────────────────────┘ └────────────┘ └──┘ └┘
src └──────────────────────┘ └────────────┘ └──┘
typ └──────────────────────┘ └────────────┘ └──┘ └┘
210
211 lemma measurable_neg_iff
212 [add_group α] [topological_add_group α] [measurable_space β] (f : β → α) :
id └───────┘ ┴ └───────────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
src └───────┘ └───────────────────┘ └──────────────┘
typ └───────┘ ┴ └───────────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
doc └───────────────────┘
213 measurable (λa, -f a) ↔ measurable f :=
id └────────┘ ┴ ┴┴ ┴ ┴ └────────┘ ┴
src └────────┘ ┴ ┴ └────────┘
typ └────────┘ ┴ ┴┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
214 iff.intro
id └───────┘
src └───────┘
typ └───────┘
215 begin
st └─────
216 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
217 have := measurable.neg h,
id └────────────┘ ┴
src └──────┘└────────────┘┴
typ └──────┘└────────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ─────────────────────────┘└─
218 convert this,
id └──┘
src └──────┘
typ └──────┘└──┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ─────────────┘└─
219 funext,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
220 simp only [pi.neg_apply, _root_.neg_neg]
id └──────────┘ └────────────┘
src └─────────┘└──────────┘└┘└────────────┘└┘
typ └─────────┘└──────────┘└┘└────────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st ──────────────────────────────────────────┘
221 end
st └─┘
222 $ measurable.neg
id └────────────┘
src └────────────┘
typ └────────────┘
223
224 lemma measurable.sub
225 [add_group α] [topological_add_group α] [second_countable_topology α] [measurable_space β]
id └───────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
src └───────┘ └───────────────────┘ └───────────────────────┘ └──────────────┘
typ └───────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
doc └───────────────────┘ └───────────────────────┘
226 {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a - g a) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
227 measurable_of_continuous2 continuous_sub
id └───────────────────────┘ └────────────┘
src └───────────────────────┘ └────────────┘
typ └───────────────────────┘ └────────────┘
228
229 lemma measurable.mul
230 [monoid α] [topological_monoid α] [second_countable_topology α] [measurable_space β]
id └────┘ ┴ └────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
src └────┘ └────────────────┘ └───────────────────────┘ └──────────────┘
typ └────┘ ┴ └────────────────┘ ┴ └───────────────────────┘ ┴ └──────────────┘ ┴
doc └────────────────┘ └───────────────────────┘
231 {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a * g a) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
232 measurable_of_continuous2 continuous_mul
id └───────────────────────┘ └────────────┘
src └───────────────────────┘ └────────────┘
typ └───────────────────────┘ └────────────┘
233
234 lemma is_measurable_le {α β}
235 [topological_space α] [partial_order α] [order_closed_topology α] [second_countable_topology α]
id └───────────────┘ ┴ └───────────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └───────────┘ └───────────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └───────────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────┘ └───────────────────────┘
236 [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └──────────────┘ └────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
237 is_measurable {a | f a ≤ g a} :=
id └───────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
238 have is_measurable {p : α × α | p.1 ≤ p.2},
id └───────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └───────────┘ ┴ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └───────────┘
239 by rw borel_prod; exact is_measurable_of_is_closed (order_closed_topology.is_closed_le' _),
id └────────┘ └────────────────────────┘ └─────────────────────────────────┘
src └─┘└────────┘ └────┘└────────────────────────┘┴ └─────────────────────────────────┘└─┘
typ └─┘└────────┘ └────┘└────────────────────────┘┴ └─────────────────────────────────┘└─┘
doc └─┘ └────┘ ┴ └─┘
txt └─┘ └────┘ ┴ └─┘
par └─┘ └────┘ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st └──────────────────────────────────────────────────────────────────────────────────────┘
240 show is_measurable {a | (f a, g a).1 ≤ (f a, g a).2},
id └───────────┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────────┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └───────────┘
241 begin
st └─────
242 refine measurable.preimage _ this,
id └─────────────────┘ └──┘
src └─────┘└─────────────────┘└─┘
typ └─────┘└─────────────────┘└─┘└──┘
doc └─────┘ └─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴ └─┘
st ──────────────────────────────────┘└─
243 exact measurable.prod_mk hf hg
id └────────────────┘ └┘ └┘
src └────┘└────────────────┘┴ ┴ ┴
typ └────┘└────────────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────┘
244 end
st └─┘
245
246 lemma measurable.max {α β}
247 [topological_space α] [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
id └───────────────┘ ┴ └────────────────────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └────────────────────┘ └───────────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └────────────────────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────┘ └───────────────────────┘
248 [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └──────────────┘ └────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
249 measurable (λa, max (f a) (g a)) :=
id └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └────────┘ └─┘
typ └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └────────┘
250 measurable.if (is_measurable_le hf hg) hg hf
id └───────────┘ └──────────────┘ └┘ └┘ └┘ └┘
src └───────────┘ └──────────────┘
typ └───────────┘ └──────────────┘ └┘ └┘ └┘ └┘
251
252 lemma measurable.min {α β}
253 [topological_space α] [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
id └───────────────┘ ┴ └────────────────────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └────────────────────┘ └───────────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └────────────────────┘ ┴ └───────────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────┘ └───────────────────────┘
254 [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └──────────────┘ └────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
255 measurable (λa, min (f a) (g a)) :=
id └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └────────┘ └─┘
typ └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └────────┘
256 measurable.if (is_measurable_le hf hg) hf hg
id └───────────┘ └──────────────┘ └┘ └┘ └┘ └┘
src └───────────┘ └──────────────┘
typ └───────────┘ └──────────────┘ └┘ └┘ └┘ └┘
257
258 -- generalize
259 lemma measurable_coe_int_real : measurable (λa, a : ℤ → ℝ) :=
id └────────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘
260 assume s (hs : is_measurable s), by trivial
id ┴ └───────────┘ ┴
src └───────────┘ └───────
typ ┴ └───────────┘ ┴ └───────
doc └───────────┘ └───────
txt └───────
par └───────
pid └
st └────────
261
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
262 section order_closed_topology
263 variables [linear_order α] [order_closed_topology α] {a b c : α}
id └──────────┘ └───────────────────┘
src └──────────┘ └───────────────────┘
typ └──────────┘ └───────────────────┘
doc └───────────────────┘
264
265 lemma is_measurable_Iio : is_measurable (Iio a) := is_measurable_of_is_open is_open_Iio
id └───────────┘ └─┘ ┴ └──────────────────────┘ └─────────┘
src └───────────┘ └─┘ └──────────────────────┘ └─────────┘
typ └───────────┘ └─┘ ┴ └──────────────────────┘ └─────────┘
doc └───────────┘ └─┘
266 lemma is_measurable_Ioi : is_measurable (Ioi a) := is_measurable_of_is_open is_open_Ioi
id └───────────┘ └─┘ ┴ └──────────────────────┘ └─────────┘
src └───────────┘ └─┘ └──────────────────────┘ └─────────┘
typ └───────────┘ └─┘ ┴ └──────────────────────┘ └─────────┘
doc └───────────┘ └─┘
267 lemma is_measurable_Ici : is_measurable (Ici a) := is_measurable_of_is_closed is_closed_Ici
id └───────────┘ └─┘ ┴ └────────────────────────┘ └───────────┘
src └───────────┘ └─┘ └────────────────────────┘ └───────────┘
typ └───────────┘ └─┘ ┴ └────────────────────────┘ └───────────┘
doc └───────────┘ └─┘
268 lemma is_measurable_Iic : is_measurable (Iic a) := is_measurable_of_is_closed is_closed_Iic
id └───────────┘ └─┘ ┴ └────────────────────────┘ └───────────┘
src └───────────┘ └─┘ └────────────────────────┘ └───────────┘
typ └───────────┘ └─┘ ┴ └────────────────────────┘ └───────────┘
doc └───────────┘ └─┘
269 lemma is_measurable_Ioo : is_measurable (Ioo a b) := is_measurable_of_is_open is_open_Ioo
id └───────────┘ └─┘ ┴ ┴ └──────────────────────┘ └─────────┘
src └───────────┘ └─┘ └──────────────────────┘ └─────────┘
typ └───────────┘ └─┘ ┴ ┴ └──────────────────────┘ └─────────┘
doc └───────────┘ └─┘
270 lemma is_measurable_Ioc : is_measurable (Ioc a b) := is_measurable_Ioi.inter is_measurable_Iic
id └───────────┘ └─┘ ┴ ┴ └───────────────┘└────┘ └───────────────┘
src └───────────┘ └─┘ └───────────────┘└────┘ └───────────────┘
typ └───────────┘ └─┘ ┴ ┴ └───────────────┘└────┘ └───────────────┘
doc └───────────┘ └─┘
271 lemma is_measurable_Ico : is_measurable (Ico a b) := is_measurable_Ici.inter is_measurable_Iio
id └───────────┘ └─┘ ┴ ┴ └───────────────┘└────┘ └───────────────┘
src └───────────┘ └─┘ └───────────────┘└────┘ └───────────────┘
typ └───────────┘ └─┘ ┴ ┴ └───────────────┘└────┘ └───────────────┘
doc └───────────┘ └─┘
272 lemma is_measurable_Icc : is_measurable (Icc a b) := is_measurable_of_is_closed is_closed_Icc
id └───────────┘ └─┘ ┴ ┴ └────────────────────────┘ └───────────┘
src └───────────┘ └─┘ └────────────────────────┘ └───────────┘
typ └───────────┘ └─┘ ┴ ┴ └────────────────────────┘ └───────────┘
doc └───────────┘ └─┘
273
274 open_locale interval
275
276 lemma is_measurable_interval
277 {α} [decidable_linear_order α] [topological_space α] [order_closed_topology α] {a b : α} :
id └────────────────────┘ ┴ └───────────────┘ ┴ └───────────────────┘ ┴ ┴
src └────────────────────┘ └───────────────┘ └───────────────────┘
typ └────────────────────┘ ┴ └───────────────┘ ┴ └───────────────────┘ ┴ ┴
doc └───────────────┘ └───────────────────┘
278 is_measurable [a, b] :=
id └───────────┘ ┴┴┴ ┴┴
src └───────────┘ ┴ ┴ ┴
typ └───────────┘ ┴┴┴ ┴┴
doc └───────────┘ ┴ ┴ ┴
279 is_measurable_Icc
id └───────────────┘
src └───────────────┘
typ └───────────────┘
280
281 end order_closed_topology
282
283 lemma measurable.is_lub {α} [topological_space α] [linear_order α]
id └───────────────┘ ┴ └──────────┘ ┴
src └───────────────┘ └──────────┘
typ └───────────────┘ ┴ └──────────┘ ┴
doc └───────────────┘
284 [order_topology α] [second_countable_topology α]
id └────────────┘ ┴ └───────────────────────┘ ┴
src └────────────┘ └───────────────────────┘
typ └────────────┘ ┴ └───────────────────────┘ ┴
doc └────────────┘ └───────────────────────┘
285 {β} [measurable_space β] {ι} [encodable ι]
id └──────────────┘ ┴ └───────┘ ┴
src └──────────────┘ └───────┘
typ └──────────────┘ ┴ └───────┘ ┴
doc └───────┘
286 {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
id ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
287 (hg : ∀ b, is_lub {a | ∃ i, f i b = a} (g b)) :
id ┴ └────┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴
typ ┴ └────┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────┘
288 measurable g :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
289 begin
st └─────
290 rw borel_eq_generate_Ioi α,
id └───────────────────┘ ┴
src └─┘└───────────────────┘┴
typ └─┘└───────────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───────────────────────────┘└─
291 apply measurable_generate_from,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────┘└─
292 rintro _ ⟨a, rfl⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ──────────────────┘└─
293 have : {b | a < g b} = ⋃ i, {b | a < f i b},
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ ┴┴┴ ┴ └┘┴┴┴└┘┴┴┴└──┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ └──┘ ┴┴┴┴┴ └┘┴┴┴└┘┴┴┴└──┘┴┴ ┴┴┴ ┴ ┴
doc └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴┴└┘┴┴ └──┘ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────┘└─
294 { simp [set.ext_iff], intro b, rw [lt_is_lub_iff (hg b)],
id └─────────┘ └───────────┘ └┘ ┴
src └────┘└─────────┘┴ └─────┘ └──┘└───────────┘┴ ┴ └┘
typ └────┘└─────────┘┴ └─────┘ └──┘└───────────┘┴ └┘┴┴└┘
doc └────┘ ┴ └─────┘ └──┘ ┴ ┴ └┘
txt └────┘ ┴ └─────┘ └──┘ ┴ ┴ └┘
par └────┘ ┴ └─────┘ └──┘ ┴ ┴ └┘
pid ┴┴ ┴ └┘ └┘ ┴ ┴ └┘
st ───┘└────────────────┘└───────┘└────────────────────────┘└──
295 exact ⟨λ ⟨_, ⟨i, rfl⟩, h⟩, ⟨i, h⟩, λ ⟨i, h⟩, ⟨_, ⟨i, rfl⟩, h⟩⟩ },
id ┴ ┴ ┴ ┴ └─┘
src └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘└─┘└─┘ └─┘
typ └────┘ └───┘ ┴└┘ └─┘┴└─┘ └┘ └─┘ └┘┴└┘┴└─┘ └─┘ └┘└─┘└─┘ └─┘
doc └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └─┘
txt └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └─┘
par └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └─┘
pid ┴ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └┘┴
st ──────────────────────────────────────────────────────────────────┘└┘└
296 show is_measurable {b | a < g b}, rw this,
id └───────────┘ ┴ ┴ ┴ └──┘
src └───┘└───────────┘┴┴└──┘ ┴ ┴ ┴ ┴ └─┘
typ └───┘└───────────┘┴┴└──┘┴┴ ┴┴┴ ┴ └─┘└──┘
doc └───┘└───────────┘┴ └──┘ ┴ ┴ ┴ ┴ └─┘
txt └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘
par └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘
pid └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└───────┘└─
297 exact is_measurable.Union (λ i, hf i _
id └─────────────────┘ └┘
src └────┘└─────────────────┘┴ └──┘ ┴ └──
typ └────┘└─────────────────┘┴ └──┘└┘┴ └──
doc └────┘ ┴ └──┘ ┴ └──
txt └────┘ ┴ └──┘ ┴ └──
par └────┘ ┴ └──┘ ┴ └──
pid ┴ ┴ └──┘ ┴ └──
st ─────────────────────────────────────────
298 (is_measurable_of_is_open (is_open_lt' _)))
id └──────────────────────┘ └─────────┘
src ───┘ └──────────────────────┘┴ └─────────┘└────┘
typ ───┘ └──────────────────────┘┴ └─────────┘└────┘
doc ───┘ ┴ └────┘
txt ───┘ ┴ └────┘
par ───┘ ┴ └────┘
pid ───┘ ┴ └───┘┴
st ───────────────────────────────────────────────┘
299 end
st └─┘
300
301 lemma measurable.is_glb {α} [topological_space α] [linear_order α]
id └───────────────┘ ┴ └──────────┘ ┴
src └───────────────┘ └──────────┘
typ └───────────────┘ ┴ └──────────┘ ┴
doc └───────────────┘
302 [order_topology α] [second_countable_topology α]
id └────────────┘ ┴ └───────────────────────┘ ┴
src └────────────┘ └───────────────────────┘
typ └────────────┘ ┴ └───────────────────────┘ ┴
doc └────────────┘ └───────────────────────┘
303 {β} [measurable_space β] {ι} [encodable ι]
id └──────────────┘ ┴ └───────┘ ┴
src └──────────────┘ └───────┘
typ └──────────────┘ ┴ └───────┘ ┴
doc └───────┘
304 {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
id ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
305 (hg : ∀ b, is_glb {a | ∃ i, f i b = a} (g b)) :
id ┴ └────┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴
typ ┴ └────┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────┘
306 measurable g :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
307 begin
st └─────
308 rw borel_eq_generate_Iio α,
id └───────────────────┘ ┴
src └─┘└───────────────────┘┴
typ └─┘└───────────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───────────────────────────┘└─
309 apply measurable_generate_from,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────┘└─
310 rintro _ ⟨a, rfl⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ──────────────────┘└─
311 have : {b | g b < a} = ⋃ i, {b | f i b < a},
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ ┴ ┴┴┴ └┘┴┴┴└┘┴┴┴└──┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ └──┘┴┴ ┴┴┴ └┘┴┴┴└┘┴┴┴└──┘┴┴ ┴ ┴ ┴┴┴
doc └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴┴└┘┴┴ └──┘ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────┘└─
312 { simp [set.ext_iff], intro b, rw [is_glb_lt_iff (hg b)],
id └─────────┘ └───────────┘ └┘ ┴
src └────┘└─────────┘┴ └─────┘ └──┘└───────────┘┴ ┴ └┘
typ └────┘└─────────┘┴ └─────┘ └──┘└───────────┘┴ └┘┴┴└┘
doc └────┘ ┴ └─────┘ └──┘ ┴ ┴ └┘
txt └────┘ ┴ └─────┘ └──┘ ┴ ┴ └┘
par └────┘ ┴ └─────┘ └──┘ ┴ ┴ └┘
pid ┴┴ ┴ └┘ └┘ ┴ ┴ └┘
st ───┘└────────────────┘└───────┘└────────────────────────┘└──
313 exact ⟨λ ⟨_, ⟨i, rfl⟩, h⟩, ⟨i, h⟩, λ ⟨i, h⟩, ⟨_, ⟨i, rfl⟩, h⟩⟩ },
id ┴ ┴ ┴ ┴ └─┘
src └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘└─┘└─┘ └─┘
typ └────┘ └───┘ ┴└┘ └─┘┴└─┘ └┘ └─┘ └┘┴└┘┴└─┘ └─┘ └┘└─┘└─┘ └─┘
doc └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └─┘
txt └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └─┘
par └────┘ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └─┘
pid ┴ └───┘ └┘ └─┘ └─┘ └┘ └─┘ └┘ └┘ └─┘ └─┘ └┘ └─┘ └┘┴
st ──────────────────────────────────────────────────────────────────┘└┘└
314 show is_measurable {b | g b < a}, rw this,
id └───────────┘ ┴ ┴ ┴ └──┘
src └───┘└───────────┘┴┴└──┘ ┴ ┴ ┴ ┴ └─┘
typ └───┘└───────────┘┴┴└──┘┴┴ ┴ ┴┴┴ └─┘└──┘
doc └───┘└───────────┘┴ └──┘ ┴ ┴ ┴ ┴ └─┘
txt └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘
par └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘
pid └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└───────┘└─
315 exact is_measurable.Union (λ i, hf i _
id └─────────────────┘ └┘
src └────┘└─────────────────┘┴ └──┘ ┴ └──
typ └────┘└─────────────────┘┴ └──┘└┘┴ └──
doc └────┘ ┴ └──┘ ┴ └──
txt └────┘ ┴ └──┘ ┴ └──
par └────┘ ┴ └──┘ ┴ └──
pid ┴ ┴ └──┘ ┴ └──
st ─────────────────────────────────────────
316 (is_measurable_of_is_open (is_open_gt' _)))
id └──────────────────────┘ └─────────┘
src ───┘ └──────────────────────┘┴ └─────────┘└────┘
typ ───┘ └──────────────────────┘┴ └─────────┘└────┘
doc ───┘ ┴ └────┘
txt ───┘ ┴ └────┘
par ───┘ ┴ └────┘
pid ───┘ ┴ └───┘┴
st ───────────────────────────────────────────────┘
317 end
st └─┘
318
319 lemma measurable.supr {α} [topological_space α] [complete_linear_order α]
id └───────────────┘ ┴ └───────────────────┘ ┴
src └───────────────┘ └───────────────────┘
typ └───────────────┘ ┴ └───────────────────┘ ┴
doc └───────────────┘ └───────────────────┘
320 [order_topology α] [second_countable_topology α]
id └────────────┘ ┴ └───────────────────────┘ ┴
src └────────────┘ └───────────────────────┘
typ └────────────┘ ┴ └───────────────────────┘ ┴
doc └────────────┘ └───────────────────────┘
321 {β} [measurable_space β] {ι} [encodable ι]
id └──────────────┘ ┴ └───────┘ ┴
src └──────────────┘ └───────┘
typ └──────────────┘ ┴ └───────┘ ┴
doc └───────┘
322 {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
323 measurable (λ b, ⨆ i, f i b) :=
id └────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └────────┘ ┴ ┴
324 measurable.is_lub hf $ λ b, is_lub_supr
id └───────────────┘ └┘ ┴ └─────────┘
src └───────────────┘ └─────────┘
typ └───────────────┘ └┘ ┴ └─────────┘
325
326 lemma measurable.infi {α} [topological_space α] [complete_linear_order α]
id └───────────────┘ ┴ └───────────────────┘ ┴
src └───────────────┘ └───────────────────┘
typ └───────────────┘ ┴ └───────────────────┘ ┴
doc └───────────────┘ └───────────────────┘
327 [order_topology α] [second_countable_topology α]
id └────────────┘ ┴ └───────────────────────┘ ┴
src └────────────┘ └───────────────────────┘
typ └────────────┘ ┴ └───────────────────────┘ ┴
doc └────────────┘ └───────────────────────┘
328 {β} [measurable_space β] {ι} [encodable ι]
id └──────────────┘ ┴ └───────┘ ┴
src └──────────────┘ └───────┘
typ └──────────────┘ ┴ └───────┘ ┴
doc └───────┘
329 {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
330 measurable (λ b, ⨅ i, f i b) :=
id └────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └────────┘ ┴ ┴
331 measurable.is_glb hf $ λ b, is_glb_infi
id └───────────────┘ └┘ ┴ └─────────┘
src └───────────────┘ └─────────┘
typ └───────────────┘ └┘ ┴ └─────────┘
332
333 lemma measurable.supr_Prop {α} [topological_space α] [complete_linear_order α]
id └───────────────┘ ┴ └───────────────────┘ ┴
src └───────────────┘ └───────────────────┘
typ └───────────────┘ ┴ └───────────────────┘ ┴
doc └───────────────┘ └───────────────────┘
334 {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f) :
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └──────────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘
335 measurable (λ b, ⨆ h : p, f b) :=
id └────────┘ ┴ ┴ ┴┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴┴ ┴ ┴
doc └────────┘ ┴ ┴
336 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
337 (assume h : p, begin convert hf, funext, exact supr_pos h end)
id ┴ └┘ └──────┘ ┴
src └──────┘ └────┘ └────┘└──────┘┴ ┴
typ ┴ └──────┘└┘ └────┘ └────┘└──────┘┴┴┴
doc └──────┘ └────┘ └────┘ ┴ ┴
txt └──────┘ └────┘ └────┘ ┴ ┴
par └──────┘ └────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └──────────────┘└──────┘└─────────────────┘└─┘
338 (assume h : ¬p, begin convert measurable_const, funext, exact supr_neg h end)
id ┴┴ └──────────────┘ └──────┘ ┴
src ┴ └──────┘└──────────────┘ └────┘ └────┘└──────┘┴ ┴
typ ┴┴ └──────┘└──────────────┘ └────┘ └────┘└──────┘┴┴┴
doc └──────┘ └────┘ └────┘ ┴ ┴
txt └──────┘ └────┘ └────┘ ┴ ┴
par └──────┘ └────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └────────────────────────────┘└──────┘└─────────────────┘└─┘
339
340 lemma measurable.infi_Prop {α} [topological_space α] [complete_linear_order α]
id └───────────────┘ ┴ └───────────────────┘ ┴
src └───────────────┘ └───────────────────┘
typ └───────────────┘ ┴ └───────────────────┘ ┴
doc └───────────────┘ └───────────────────┘
341 {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f) :
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └──────────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘
342 measurable (λ b, ⨅ h : p, f b) :=
id └────────┘ ┴ ┴ ┴┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴┴ ┴ ┴
doc └────────┘ ┴ ┴
343 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
344 (assume h : p, begin convert hf, funext, exact infi_pos h end )
id ┴ └┘ └──────┘ ┴
src └──────┘ └────┘ └────┘└──────┘┴ ┴
typ ┴ └──────┘└┘ └────┘ └────┘└──────┘┴┴┴
doc └──────┘ └────┘ └────┘ ┴ ┴
txt └──────┘ └────┘ └────┘ ┴ ┴
par └──────┘ └────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └──────────────┘└──────┘└─────────────────┘└─┘
345 (assume h : ¬p, begin convert measurable_const, funext, exact infi_neg h end)
id ┴┴ └──────────────┘ └──────┘ ┴
src ┴ └──────┘└──────────────┘ └────┘ └────┘└──────┘┴ ┴
typ ┴┴ └──────┘└──────────────┘ └────┘ └────┘└──────┘┴┴┴
doc └──────┘ └────┘ └────┘ ┴ ┴
txt └──────┘ └────┘ └────┘ ┴ ┴
par └──────┘ └────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └────────────────────────────┘└──────┘└─────────────────┘└─┘
346
347 end
348
349 def homemorph.to_measurable_equiv [topological_space α] [topological_space β] (h : α ≃ₜ β) :
id └───────────────┘ ┴ └───────────────┘ ┴ ┴ └┘ ┴
src └───────────────┘ └───────────────┘ └┘
typ └───────────────┘ ┴ └───────────────┘ ┴ ┴ └┘ ┴
doc └───────────────┘ └───────────────┘ └┘
350 measurable_equiv α β :=
id └──────────────┘ ┴ ┴
src └──────────────┘
typ └──────────────┘ ┴ ┴
doc └──────────────┘
351 { to_equiv := h.to_equiv,
id ┴└───────┘
src └───────┘
typ ┴└───────┘
352 measurable_to_fun := measurable_of_continuous h.continuous_to_fun,
id └──────────────────────┘ ┴└────────────────┘
src └──────────────────────┘ └────────────────┘
typ └──────────────────────┘ ┴└────────────────┘
353 measurable_inv_fun := measurable_of_continuous h.continuous_inv_fun }
id └──────────────────────┘ ┴└─────────────────┘
src └──────────────────────┘ └─────────────────┘
typ └──────────────────────┘ ┴└─────────────────┘
354
355 namespace real
356 open measurable_space
357
358 lemma borel_eq_generate_from_Ioo_rat :
359 borel ℝ = generate_from (⋃(a b : ℚ) (h : a < b), {Ioo a b}) :=
id └───┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─┘ ┴ ┴
src └───┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴└─┘
typ └───┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─┘ ┴ ┴
doc └───────────┘ ┴ ┴ ┴ └─┘
360 borel_eq_generate_from_of_subbasis is_topological_basis_Ioo_rat.2.2
id └────────────────────────────────┘ └──────────────────────────┘┴ ┴
src └────────────────────────────────┘ └──────────────────────────┘┴ ┴
typ └────────────────────────────────┘ └──────────────────────────┘┴ ┴
361
362 lemma borel_eq_generate_from_Iio_rat :
363 borel ℝ = generate_from (⋃a:ℚ, {Iio a}) :=
id └───┘ ┴ ┴ └───────────┘ ┴ ┴┴ ┴└─┘ ┴
src └───┘ ┴ ┴ └───────────┘ ┴ ┴┴ ┴└─┘
typ └───┘ ┴ ┴ └───────────┘ ┴ ┴┴ ┴└─┘ ┴
doc └───────────┘ ┴ ┴┴ └─┘
364 begin
st └─────
365 let g, swap,
src └───┘ └──┘
typ └───┘ └──┘
doc └───┘ └──┘
txt └───┘ └──┘
par └───┘ └──┘
pid └───┘
st ──────┘└────┘└─
366 apply le_antisymm (_ : _ ≤ g) (measurable_space.generate_from_le (λ t, _)),
id └─────────┘ ┴ ┴ └───────────────────────────────┘
src └────┘└─────────┘┴ └────┘┴┴ └┘ └───────────────────────────────┘┴ └─────┘
typ └────┘└─────────┘┴ └────┘┴┴┴└┘ └───────────────────────────────┘┴ └─────┘
doc └────┘ ┴ └────┘ ┴ └┘ ┴ └─────┘
txt └────┘ ┴ └────┘ ┴ └┘ ┴ └─────┘
par └────┘ ┴ └────┘ ┴ └┘ ┴ └─────┘
pid ┴ ┴ └────┘ ┴ └┘ ┴ └─────┘
st ───────────────────────────────────────────────────────────────────────────┘└─
367 { rw borel_eq_generate_from_Ioo_rat,
id └────────────────────────────┘
src └─┘└────────────────────────────┘
typ └─┘└────────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└───────────────────────────────┘└─
368 refine generate_from_le (λ t, _),
id └──────────────┘
src └─────┘└──────────────┘┴ └────┘
typ └─────┘└──────────────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ───────────────────────────────────┘└─
369 simp only [mem_Union], rintro ⟨a, b, h, rfl|⟨⟨⟩⟩⟩,
id └───────┘
src └─────────┘└───────┘┴ └────────────────────────┘
typ └─────────┘└───────┘┴ └────────────────────────┘
doc └─────────┘ ┴ └────────────────────────┘
txt └─────────┘ ┴ └────────────────────────┘
par └─────────┘ ┴ └────────────────────────┘
pid ┴└──┘└┘ ┴ └──────────────────┘
st ────────────────────────┘└──────────────────────────┘└─
370 rw (set.ext (λ x, _) : Ioo (a:ℝ) b = (⋃c>a, - Iio c) ∩ Iio b),
id └─────┘ └─┘ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴
src └─┘ └─────┘┴ └───────┘└─┘┴ ┴ └┘ ┴┴┴ ┴└┘ ┴┴┴┴ ┴ └┘┴┴└─┘┴ ┴
typ └─┘ └─────┘┴ └───────┘└─┘┴ ┴ └┘ ┴┴┴ ┴└┘┴┴┴┴┴ ┴ └┘┴┴└─┘┴┴┴
doc └─┘ ┴ └───────┘└─┘┴ ┴ └┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ └┘ ┴└─┘┴ ┴
txt └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────┘└─
371 { have hg : ∀q:ℚ, g.is_measurable (Iio q) :=
id └─────────────┘ └─┘
src └────────┘ └┘ ┴└─────────────┘┴ └─┘┴ └────
typ └────────┘ └┘ ┴└─────────────┘┴ └─┘┴ └────
doc └────────┘ └┘ ┴ ┴ └─┘┴ └────
txt └────────┘ └┘ ┴ ┴ ┴ └────
par └────────┘ └┘ ┴ ┴ ┴ └────
pid └─────┘└─┘ └┘ ┴ ┴ ┴ ┴└───
st ─────┘└──────────────────────────────────────────
372 λ q, generate_measurable.basic _ (by simp; exact ⟨_, rfl⟩),
id └───────────────────────┘ └─┘
src ───────┘ └──┘└───────────────────────┘└─┘ ┴└──┘└┘└────┘ └─┘└─┘┴┴
typ ───────┘ └──┘└───────────────────────┘└─┘ ┴└──┘└┘└────┘ └─┘└─┘┴┴
doc ───────┘ └──┘ └─┘ ┴└──┘└┘└────┘ └─┘ ┴┴
txt ───────┘ └──┘ └─┘ ┴└──┘└┘└────┘ └─┘ ┴┴
par ───────┘ └──┘ └─┘ ┴└──┘└┘└────┘ └─┘ ┴┴
pid ───────┘ └──┘ └─┘ └───────────┘ └─┘ └┘
st ───────────────────────────────────────────┘└───────────────────┘┴└─
373 refine @is_measurable.inter _ g _ _ _ (hg _),
id └─────────────────┘ ┴ └┘
src └─────┘ └─────────────────┘└─┘ └─────┘ └─┘
typ └─────┘ └─────────────────┘└─┘┴└─────┘ └┘└─┘
doc └─────┘ └─┘ └─────┘ └─┘
txt └─────┘ └─┘ └─────┘ └─┘
par └─────┘ └─┘ └─────┘ └─┘
pid ┴ └─┘ └─────┘ └─┘
st ─────────────────────────────────────────────────┘└─
374 refine @is_measurable.bUnion _ _ g _ _ (countable_encodable _) (λ c h, _),
id └──────────────────┘ ┴ └─────────────────┘
src └─────┘ └──────────────────┘└───┘ └───┘ └─────────────────┘└──┘ └──────┘
typ └─────┘ └──────────────────┘└───┘┴└───┘ └─────────────────┘└──┘ └──────┘
doc └─────┘ └───┘ └───┘ └──┘ └──────┘
txt └─────┘ └───┘ └───┘ └──┘ └──────┘
par └─────┘ └───┘ └───┘ └──┘ └──────┘
pid ┴ └───┘ └───┘ └──┘ └──────┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
375 exact @is_measurable.compl _ _ g (hg _) },
id └─────────────────┘ ┴ └┘
src └────┘ └─────────────────┘└───┘ ┴ └──┘
typ └────┘ └─────────────────┘└───┘┴┴ └┘└──┘
doc └────┘ └───┘ ┴ └──┘
txt └────┘ └───┘ ┴ └──┘
par └────┘ └───┘ ┴ └──┘
pid ┴ └───┘ ┴ └─┘┴
st ─────────────────────────────────────────────┘└┘└
376 { simp [Ioo, Iio],
id └─┘ └─┘
src └────┘└─┘└┘└─┘┴
typ └────┘└─┘└┘└─┘┴
doc └────┘└─┘└┘└─┘┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────┘└─
377 refine and_congr _ iff.rfl,
id └───────┘ └─────┘
src └─────┘└───────┘└─┘└─────┘
typ └─────┘└───────┘└─┘└─────┘
doc └─────┘ └─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴ └─┘
st ───────────────────────────────┘└─
378 exact ⟨λ h,
src └────┘ └───
typ └────┘ └───
doc └────┘ └───
txt └────┘ └───
par └────┘ └───
pid ┴ └───
st ──────────────────
379 let ⟨c, ac, cx⟩ := exists_rat_btwn h in
id ┴ └┘ └┘ └─────────────┘
src ───────┘ ┴ └┘ └┘ └───┘└─────────────┘┴ └───
typ ───────┘ ┴ ┴└┘└┘└┘└┘└───┘└─────────────┘┴ └───
doc ───────┘ ┴ └┘ └┘ └───┘ ┴ └───
txt ───────┘ ┴ └┘ └┘ └───┘ ┴ └───
par ───────┘ ┴ └┘ └┘ └───┘ ┴ └───
pid ───────┘ ┴ └┘ └┘ └───┘ ┴ └───
st ────────────────────────────────────────────────
380 ⟨c, rat.cast_lt.1 ac, le_of_lt cx⟩,
id └──────┘
src ───────┘ └┘ └─┘ └┘└──────┘┴ └──
typ ───────┘ └┘ └─┘ └┘└──────┘┴ └──
doc ───────┘ └┘ └─┘ └┘ ┴ └──
txt ───────┘ └┘ └─┘ └┘ ┴ └──
par ───────┘ └┘ └─┘ └┘ ┴ └──
pid ───────┘ └┘ └─┘ └┘ ┴ └──
st ────────────────────────────────────────────
381 λ ⟨c, ac, cx⟩, lt_of_lt_of_le (rat.cast_lt.2 ac) cx⟩ } },
id └┘ └┘ └────────────┘ └─────────┘
src ──────┘ └┘ └┘ └┘ └─┘└────────────┘┴ └─────────┘└─┘ └┘ └┘
typ ──────┘ └┘ └┘└┘└┘└┘└─┘└────────────┘┴ └─────────┘└─┘ └┘ └┘
doc ──────┘ └┘ └┘ └┘ └─┘ ┴ └─┘ └┘ └┘
txt ──────┘ └┘ └┘ └┘ └─┘ ┴ └─┘ └┘ └┘
par ──────┘ └┘ └┘ └┘ └─┘ ┴ └─┘ └┘ └┘
pid ──────┘ └┘ └┘ └┘ └─┘ ┴ └─┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────┘└──┘└
382 { simp, rintro r rfl,
src └──┘ └──────────┘
typ └──┘ └──────────┘
doc └──┘ └──────────┘
txt └──┘ └──────────┘
par └──┘ └──────────┘
pid └────┘
st ───────┘└────────────┘└─
383 exact is_measurable_of_is_open (is_open_gt' _) }
id └──────────────────────┘ └─────────┘
src └────┘└──────────────────────┘┴ └─────────┘└──┘
typ └────┘└──────────────────────┘┴ └─────────┘└──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └─┘┴
st ──────────────────────────────────────────────────┘└─
384 end
st ──┘
385
386 end real
387
388 namespace nnreal
389 open filter
390
391 lemma measurable.add [measurable_space α] {f : α → nnreal} {g : α → nnreal} :
id └──────────────┘ ┴ ┴ └────┘ ┴ └────┘
src └──────────────┘ └────┘ └────┘
typ └──────────────┘ ┴ ┴ └────┘ ┴ └────┘
doc └────┘ └────┘
392 measurable f → measurable g → measurable (λa, f a + g a) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
393 measurable_of_continuous2 continuous_add
id └───────────────────────┘ └────────────┘
src └───────────────────────┘ └────────────┘
typ └───────────────────────┘ └────────────┘
394
395 lemma measurable.sub [measurable_space α] {f g: α → nnreal}
id └──────────────┘ ┴ ┴ └────┘
src └──────────────┘ └────┘
typ └──────────────┘ ┴ ┴ └────┘
doc └────┘
396 (hf : measurable f) (hg : measurable g) : measurable (λ a, f a - g a) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
397 measurable_of_continuous2 continuous_sub hf hg
id └───────────────────────┘ └────────────┘ └┘ └┘
src └───────────────────────┘ └────────────┘
typ └───────────────────────┘ └────────────┘ └┘ └┘
398
399 lemma measurable.mul [measurable_space α] {f : α → nnreal} {g : α → nnreal} :
id └──────────────┘ ┴ ┴ └────┘ ┴ └────┘
src └──────────────┘ └────┘ └────┘
typ └──────────────┘ ┴ ┴ └────┘ ┴ └────┘
doc └────┘ └────┘
400 measurable f → measurable g → measurable (λa, f a * g a) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
401 measurable_of_continuous2 continuous_mul
id └───────────────────────┘ └────────────┘
src └───────────────────────┘ └────────────┘
typ └───────────────────────┘ └────────────┘
402
403 lemma measurable_of_real : measurable nnreal.of_real :=
id └────────┘ └────────────┘
src └────────┘ └────────────┘
typ └────────┘ └────────────┘
doc └────────┘
404 measurable_of_continuous nnreal.continuous_of_real
id └──────────────────────┘ └───────────────────────┘
src └──────────────────────┘ └───────────────────────┘
typ └──────────────────────┘ └───────────────────────┘
405
406 end nnreal
407
408 namespace ennreal
409 open filter
410
411 lemma measurable_coe : measurable (coe : nnreal → ennreal) :=
id └────────┘ └─┘ └────┘ └─────┘
src └────────┘ └─┘ └────┘ └─────┘
typ └────────┘ └─┘ └────┘ └─────┘
doc └────────┘ └────┘ └─────┘
412 measurable_of_continuous (continuous_coe.2 continuous_id)
id └──────────────────────┘ └────────────┘┴ └───────────┘
src └──────────────────────┘ └────────────┘┴ └───────────┘
typ └──────────────────────┘ └────────────┘┴ └───────────┘
413
414 def ennreal_equiv_nnreal : measurable_equiv {r : ennreal | r < ⊤} nnreal :=
id └──────────────┘ ┴ └─────┘ ┴ ┴ ┴ └────┘
src └──────────────┘ ┴ └─────┘ ┴ ┴ └────┘
typ └──────────────┘ ┴ └─────┘ ┴ ┴ ┴ └────┘
doc └──────────────┘ └─────┘ └────┘
415 { to_fun := λr, ennreal.to_nnreal r.1,
id ┴ └───────────────┘ ┴┴
src └───────────────┘ ┴
typ ┴ └───────────────┘ ┴┴
doc └───────────────┘
416 inv_fun := λr, ⟨r, coe_lt_top⟩,
id ┴ ┴ └────────┘
src └────────┘
typ ┴ ┴ └────────┘
417 left_inv := assume ⟨r, hr⟩, by simp [coe_to_nnreal (ne_of_lt hr)],
id ┴ └───────────┘ └──────┘ └┘
src └────┘└───────────┘┴ └──────┘┴ └┘
typ ┴ └────┘└───────────┘┴ └──────┘┴└┘└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴┴ ┴ ┴ └┘
st └─────────────────────────────────┘
418 right_inv := assume r, to_nnreal_coe,
id ┴ └───────────┘
src └───────────┘
typ ┴ └───────────┘
419 measurable_to_fun :=
420 begin
st └─────
421 rw [← borel_eq_subtype],
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st ─────────────────────────┘└──
422 refine measurable_of_continuous (continuous_iff_continuous_at.2 _),
id └──────────────────────┘ └──────────────────────────┘
src └─────┘└──────────────────────┘┴ └──────────────────────────┘└───┘
typ └─────┘└──────────────────────┘┴ └──────────────────────────┘└───┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ─────────────────────────────────────────────────────────────────────┘└─
423 rintros ⟨r, hr⟩,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └──────┘
st ──────────────────┘└─
424 simp [continuous_at, nhds_subtype_eq_comap],
id └───────────┘ └───────────────────┘
src └────┘└───────────┘└┘└───────────────────┘┴
typ └────┘└───────────┘└┘└───────────────────┘┴
doc └────┘└───────────┘└┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ──────────────────────────────────────────────┘└─
425 refine tendsto.comp (tendsto_to_nnreal (ne_of_lt hr)) tendsto_comap
id └──────────┘ └───────────────┘ └──────┘ └┘ └───────────┘
src └─────┘└──────────┘┴ └───────────────┘┴ └──────┘┴ └─┘└───────────┘└
typ └─────┘└──────────┘┴ └───────────────┘┴ └──────┘┴└┘└─┘└───────────┘└
doc └─────┘ ┴ ┴ ┴ └─┘ └
txt └─────┘ ┴ ┴ ┴ └─┘ └
par └─────┘ ┴ ┴ ┴ └─┘ └
pid ┴ ┴ ┴ ┴ └─┘ └
st ────────────────────────────────────────────────────────────────────────
426 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
427 measurable_inv_fun := measurable.subtype_mk measurable_coe }
id └───────────────────┘ └────────────┘
src └───────────────────┘ └────────────┘
typ └───────────────────┘ └────────────┘
428
429 lemma measurable_of_measurable_nnreal [measurable_space α] {f : ennreal → α}
id └──────────────┘ ┴ └─────┘ ┴
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ └─────┘ ┴
doc └─────┘
430 (h : measurable (λp:nnreal, f p)) : measurable f :=
id └────────┘ └────┘ ┴ ┴ └────────┘ ┴
src └────────┘ └────┘ └────────┘
typ └────────┘ └────┘ ┴ ┴ └────────┘ ┴
doc └────────┘ └────┘ └────────┘
431 begin
st └─────
432 refine measurable_of_measurable_union_cover {⊤} {r : ennreal | r < ⊤}
id └──────────────────────────────────┘ ┴┴ ┴ └─────┘ ┴
src └─────┘└──────────────────────────────────┘┴┴┴└┘┴└──┘└─────┘└─┘ ┴┴┴ └─
typ └─────┘└──────────────────────────────────┘┴┴┴└┘┴└──┘└─────┘└─┘ ┴┴┴ └─
doc └─────┘ ┴ └┘ └──┘└─────┘└─┘ ┴ ┴ └─
txt └─────┘ ┴ └┘ └──┘ └─┘ ┴ ┴ └─
par └─────┘ ┴ └┘ └──┘ └─┘ ┴ ┴ └─
pid ┴ ┴ └┘ └──┘ └─┘ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────────
433 (is_measurable_of_is_closed $ is_closed_singleton)
id └────────────────────────┘ └─────────────────┘
src ───┘ └────────────────────────┘┴ ┴└─────────────────┘└─
typ ───┘ └────────────────────────┘┴ ┴└─────────────────┘└─
doc ───┘ ┴ ┴ └─
txt ───┘ ┴ ┴ └─
par ───┘ ┴ ┴ └─
pid ───┘ ┴ ┴ └─
st ───────────────────────────────────────────────────────
434 (is_measurable_of_is_open $ is_open_gt' _)
id └──────────────────────┘ └─────────┘
src ───┘ └──────────────────────┘┴ ┴└─────────┘└───
typ ───┘ └──────────────────────┘┴ ┴└─────────┘└───
doc ───┘ ┴ ┴ └───
txt ───┘ ┴ ┴ └───
par ───┘ ┴ ┴ └───
pid ───┘ ┴ ┴ └───
st ───────────────────────────────────────────────
435 (assume r _, by cases r; simp [ennreal.none_eq_top, ennreal.some_eq_coe])
id ┴ └─────────────────┘ └─────────────────┘
src ───┘ └────┘ ┴└────┘ └┘└────┘└─────────────────┘└┘└─────────────────┘┴└─
typ ───┘ └────┘ ┴└────┘┴└┘└────┘└─────────────────┘└┘└─────────────────┘┴└─
doc ───┘ └────┘ ┴└────┘ └┘└────┘ └┘ ┴└─
txt ───┘ └────┘ ┴└────┘ └┘└────┘ └┘ ┴└─
par ───┘ └────┘ ┴└────┘ └┘└────┘ └┘ ┴└─
pid ───┘ └────┘ └─────┘ └──────┘ └┘ └──
st ──────────────────┘└───────────────────────────────────────────────────────┘└─
436 _
src ──────
typ ──────
doc ──────
txt ──────
par ──────
pid ──────
st ──────
437 _,
src ────┘
typ ────┘
doc ────┘
txt ────┘
par ────┘
pid ────┘
st ────┘└─
438 exact (measurable_equiv.set.singleton ⊤).symm.measurable_coe_iff.1 (measurable_unit _),
id └────────────────────────────┘ └─────────────┘
src └────┘ └────────────────────────────┘┴ └──────────────────────────┘ └─────────────┘└─┘
typ └────┘ └────────────────────────────┘┴ └──────────────────────────┘ └─────────────┘└─┘
doc └────┘ ┴ └──────────────────────────┘ └─┘
txt └────┘ ┴ └──────────────────────────┘ └─┘
par └────┘ ┴ └──────────────────────────┘ └─┘
pid ┴ ┴ └──────────────────────────┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
439 exact (ennreal_equiv_nnreal.symm.measurable_coe_iff.1 h)
id └──────────────────────────────────────────┘ ┴
src └────┘ └──────────────────────────────────────────┘└─┘ └┘
typ └────┘ └──────────────────────────────────────────┘└─┘┴└┘
doc └────┘ └─┘ └┘
txt └────┘ └─┘ └┘
par └────┘ └─┘ └┘
pid ┴ └─┘ ┴┴
st ──────────────────────────────────────────────────────────┘
440 end
st └─┘
441
442 def ennreal_equiv_sum :
443 @measurable_equiv ennreal (nnreal ⊕ unit) _ sum.measurable_space :=
id └──────────────┘ └─────┘ └────┘ ┴ └──┘ └──────────────────┘
src └──────────────┘ └─────┘ └────┘ ┴ └──┘ └──────────────────┘
typ └──────────────┘ └─────┘ └────┘ ┴ └──┘ └──────────────────┘
doc └──────────────┘ └─────┘ └────┘ └──┘
444 { to_fun :=
445 @option.rec nnreal (λ_, nnreal ⊕ unit) (sum.inr ()) (sum.inl : nnreal → nnreal ⊕ unit),
id └────────┘ └────┘ ┴ └────┘ ┴ └──┘ └─────┘ └┘ └─────┘ └────┘ └────┘ ┴ └──┘
src └────────┘ └────┘ └────┘ ┴ └──┘ └─────┘ └┘ └─────┘ └────┘ └────┘ ┴ └──┘
typ └────────┘ └────┘ ┴ └────┘ ┴ └──┘ └─────┘ └┘ └─────┘ └────┘ └────┘ ┴ └──┘
doc └────┘ └────┘ └──┘ └────┘ └────┘ └──┘
446 inv_fun :=
447 @sum.rec nnreal unit (λ_, ennreal) (coe : nnreal → ennreal) (λ_, ⊤),
id └─────┘ └────┘ └──┘ ┴ └─────┘ └─┘ └────┘ └─────┘ ┴ ┴
src └─────┘ └────┘ └──┘ └─────┘ └─┘ └────┘ └─────┘ ┴
typ └─────┘ └────┘ └──┘ ┴ └─────┘ └─┘ └────┘ └─────┘ ┴ ┴
doc └────┘ └──┘ └─────┘ └────┘ └─────┘
448 left_inv := assume s, by cases s; refl,
id ┴ ┴
src └────┘ └──┘
typ ┴ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
449 right_inv := assume s, by rcases s with r | ⟨⟨⟩⟩; refl,
id ┴ ┴
src └─────┘ └────────────┘ └──┘
typ ┴ └─────┘┴└────────────┘ └──┘
doc └─────┘ └────────────┘ └──┘
txt └─────┘ └────────────┘ └──┘
par └─────┘ └────────────┘ └──┘
pid ┴ └────────────┘
st └───────────────────────────┘
450 measurable_to_fun := measurable_of_measurable_nnreal measurable_inl,
id └─────────────────────────────┘ └────────────┘
src └─────────────────────────────┘ └────────────┘
typ └─────────────────────────────┘ └────────────┘
451 measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ennreal unit _ _ ⊤) }
id └────────────┘ └────────────┘ └──────────────┘ └─────┘ └──┘ ┴
src └────────────┘ └────────────┘ └──────────────┘ └─────┘ └──┘ ┴
typ └────────────┘ └────────────┘ └──────────────┘ └─────┘ └──┘ ┴
doc └─────┘ └──┘
452
453 lemma measurable_of_measurable_nnreal_nnreal [measurable_space α] [measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
454 (f : ennreal → ennreal → β) {g : α → ennreal} {h : α → ennreal}
id └─────┘ └─────┘ ┴ ┴ └─────┘ ┴ └─────┘
src └─────┘ └─────┘ └─────┘ └─────┘
typ └─────┘ └─────┘ ┴ ┴ └─────┘ ┴ └─────┘
doc └─────┘ └─────┘ └─────┘ └─────┘
455 (h₁ : measurable (λp:nnreal × nnreal, f p.1 p.2))
id └────────┘ └────┘ ┴ └────┘ ┴ ┴┴ ┴┴
src └────────┘ └────┘ ┴ └────┘ ┴ ┴
typ └────────┘ └────┘ ┴ └────┘ ┴ ┴┴ ┴┴
doc └────────┘ └────┘ └────┘
456 (h₂ : measurable (λr:nnreal, f ⊤ r))
id └────────┘ └────┘ ┴ ┴ ┴
src └────────┘ └────┘ ┴
typ └────────┘ └────┘ ┴ ┴ ┴
doc └────────┘ └────┘
457 (h₃ : measurable (λr:nnreal, f r ⊤))
id └────────┘ └────┘ ┴ ┴ ┴
src └────────┘ └────┘ ┴
typ └────────┘ └────┘ ┴ ┴ ┴
doc └────────┘ └────┘
458 (hg : measurable g) (hh : measurable h) : measurable (λa, f (g a) (h a)) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
459 let e : measurable_equiv (ennreal × ennreal)
id └──────────────┘ └─────┘ ┴ └─────┘
src └──────────────┘ └─────┘ ┴ └─────┘
typ └──────────────┘ └─────┘ ┴ └─────┘
doc └──────────────┘ └─────┘ └─────┘
460 (((nnreal × nnreal) ⊕ (nnreal × unit)) ⊕ ((unit × nnreal) ⊕ (unit × unit))) :=
id └────┘ ┴ └────┘ ┴ └────┘ ┴ └──┘ ┴ └──┘ ┴ └────┘ ┴ └──┘ ┴ └──┘
src └────┘ ┴ └────┘ ┴ └────┘ ┴ └──┘ ┴ └──┘ ┴ └────┘ ┴ └──┘ ┴ └──┘
typ └────┘ ┴ └────┘ ┴ └────┘ ┴ └──┘ ┴ └──┘ ┴ └────┘ ┴ └──┘ ┴ └──┘
doc └────┘ └────┘ └────┘ └──┘ └──┘ └────┘ └──┘ └──┘
461 (measurable_equiv.prod_congr ennreal_equiv_sum ennreal_equiv_sum).trans
id └─────────────────────────┘ └───────────────┘ └───────────────┘ └───┘
src └─────────────────────────┘ └───────────────┘ └───────────────┘ └───┘
typ └─────────────────────────┘ └───────────────┘ └───────────────┘ └───┘
462 (measurable_equiv.sum_prod_sum _ _ _ _) in
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
463 have measurable (λp:ennreal×ennreal, f p.1 p.2),
id └────────┘ └─────┘┴└─────┘ ┴ ┴┴ ┴┴
src └────────┘ └─────┘┴└─────┘ ┴ ┴
typ └────────┘ └─────┘┴└─────┘ ┴ ┴┴ ┴┴
doc └────────┘ └─────┘ └─────┘
464 begin
st └─────
465 refine e.symm.measurable_coe_iff.1 (measurable_sum (measurable_sum _ _) (measurable_sum _ _)),
id └───────────────────────┘ └────────────┘
src └─────┘└───────────────────────┘└─┘ ┴ └────┘ └────────────┘└────┘
typ └─────┘└───────────────────────┘└─┘ ┴ └────┘ └────────────┘└────┘
doc └─────┘ └─┘ ┴ └────┘ └────┘
txt └─────┘ └─┘ ┴ └────┘ └────┘
par └─────┘ └─┘ ┴ └────┘ └────┘
pid ┴ └─┘ ┴ └────┘ └────┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
466 { show measurable (λp:nnreal × nnreal, f p.1 p.2),
id └────────┘ ┴ └────┘ ┴
src └───┘└────────┘┴ └┘ ┴┴┴└────┘└┘ ┴ └─┘ └─┘
typ └───┘└────────┘┴ └┘ ┴┴┴└────┘└┘┴┴ └─┘ └─┘
doc └───┘└────────┘┴ └┘ ┴ ┴└────┘└┘ ┴ └─┘ └─┘
txt └───┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └─┘
par └───┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └─┘
pid └───┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ └─┘
st ───┘└─────────────────────────────────────────────┘└─
467 exact h₁ },
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────┘└┘└
468 { show measurable (λp:nnreal × unit, f p.1 ⊤),
id └────────┘ └────┘ ┴ └──┘ ┴ ┴
src └───┘└────────┘┴ └┘└────┘┴ ┴└──┘└┘ ┴ └─┘┴┴
typ └───┘└────────┘┴ └┘└────┘┴┴┴└──┘└┘┴┴ └─┘┴┴
doc └───┘└────────┘┴ └┘└────┘┴ ┴└──┘└┘ ┴ └─┘ ┴
txt └───┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
par └───┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
pid └───┘ ┴ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
st ───┘└─────────────────────────────────────────┘└─
469 exact h₃.comp (measurable.fst measurable_id) },
id └─────┘ └────────────┘ └───────────┘
src └────┘└─────┘┴ └────────────┘┴└───────────┘└┘
typ └────┘└─────┘┴ └────────────┘┴└───────────┘└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ────────────────────────────────────────────────┘└┘└
470 { show measurable ((λp:nnreal, f ⊤ p) ∘ (λp:unit × nnreal, p.2)),
id └────────┘ ┴ ┴ └──┘ ┴ └────┘
src └───┘└────────┘┴ └┘ └┘ ┴ ┴ └┘┴┴ └┘└──┘┴ ┴└────┘└┘ └──┘
typ └───┘└────────┘┴ └┘ └┘┴┴ ┴ └┘┴┴ └┘└──┘┴┴┴└────┘└┘ └──┘
doc └───┘└────────┘┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘└──┘┴ ┴└────┘└┘ └──┘
txt └───┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └──┘
par └───┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └──┘
pid └───┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └──┘
st ───┘└────────────────────────────────────────────────────────────┘└─
471 exact h₂.comp (measurable.snd measurable_id) },
id └─────┘ └────────────┘ └───────────┘
src └────┘└─────┘┴ └────────────┘┴└───────────┘└┘
typ └────┘└─────┘┴ └────────────┘┴└───────────┘└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ────────────────────────────────────────────────┘└┘└
472 { show measurable (λp:unit × unit, f ⊤ ⊤),
id └────────┘ ┴ └──┘ ┴
src └───┘└────────┘┴ └┘ ┴ ┴└──┘└┘ ┴ ┴ ┴
typ └───┘└────────┘┴ └┘ ┴┴┴└──┘└┘┴┴ ┴ ┴
doc └───┘└────────┘┴ └┘ ┴ ┴└──┘└┘ ┴ ┴ ┴
txt └───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
par └───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
473 exact measurable_const }
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────┘└─
474 end,
st ──┘
475 this.comp (measurable.prod_mk hg hh)
id └──┘└───┘ └────────────────┘ └┘ └┘
src └───┘ └────────────────┘
typ └──┘└───┘ └────────────────┘ └┘ └┘
476
477 lemma measurable.mul {α : Type*} [measurable_space α] {f g : α → ennreal} :
id └──────────────┘ ┴ ┴ └─────┘
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ ┴ └─────┘
doc └─────┘
478 measurable f → measurable g → measurable (λa, f a * g a) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
479 begin
st └─────
480 refine measurable_of_measurable_nnreal_nnreal (*) _ _ _,
id └────────────────────────────────────┘ ┴
src └─────┘└────────────────────────────────────┘┴┴└──────┘
typ └─────┘└────────────────────────────────────┘┴┴└──────┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ────────────────────────────────────────────────────────┘└─
481 { simp only [ennreal.coe_mul.symm],
src └─────────┘ ┴
typ └─────────┘└──────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───┘└──────────────────────────────┘└─
482 exact measurable_coe.comp
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ──────────────────────────────
483 (measurable.mul (measurable.fst measurable_id) (measurable.snd measurable_id)) },
id └────────────┘ └────────────┘ └────────────┘ └───────────┘
src ─────┘ └────────────┘┴ └────────────┘┴ └┘ └────────────┘┴└───────────┘└─┘
typ ─────┘ └────────────┘┴ └────────────┘┴ └┘ └────────────┘┴└───────────┘└─┘
doc ─────┘ ┴ ┴ └┘ ┴ └─┘
txt ─────┘ ┴ ┴ └┘ ┴ └─┘
par ─────┘ ┴ ┴ └┘ ┴ └─┘
pid ─────┘ ┴ ┴ └┘ ┴ └┘┴
st ────────────────────────────────────────────────────────────────────────────────────┘└┘└
484 { simp [top_mul],
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───┘└────────────┘└─
485 exact measurable.if
id └───────────┘
src └────┘└───────────┘└
typ └────┘└───────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────
486 (is_measurable_of_is_closed $ is_closed_eq continuous_id continuous_const)
id └────────────────────────┘ └──────────┘ └───────────┘ └──────────────┘
src ─────┘ └────────────────────────┘┴ ┴└──────────┘┴└───────────┘┴└──────────────┘└─
typ ─────┘ └────────────────────────┘┴ ┴└──────────┘┴└───────────┘┴└──────────────┘└─
doc ─────┘ ┴ ┴ ┴ ┴ └─
txt ─────┘ ┴ ┴ ┴ ┴ └─
par ─────┘ ┴ ┴ ┴ ┴ └─
pid ─────┘ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────────────────────────────────────
487 measurable_const
src ─────┘ └
typ ─────┘ └
doc ─────┘ └
txt ─────┘ └
par ─────┘ └
pid ─────┘ └
st ───────────────────────
488 measurable_const },
id └──────────────┘
src ─────┘└──────────────┘┴
typ ─────┘└──────────────┘┴
doc ─────┘ ┴
txt ─────┘ ┴
par ─────┘ ┴
pid ─────┘ ┴
st ──────────────────────┘└┘└
489 { simp [mul_top],
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ─────────────────┘└─
490 exact measurable.if
id └───────────┘
src └────┘└───────────┘└
typ └────┘└───────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────
491 (is_measurable_of_is_closed $ is_closed_eq continuous_id continuous_const)
id └────────────────────────┘ └──────────┘ └───────────┘ └──────────────┘
src ─────┘ └────────────────────────┘┴ ┴└──────────┘┴└───────────┘┴└──────────────┘└─
typ ─────┘ └────────────────────────┘┴ ┴└──────────┘┴└───────────┘┴└──────────────┘└─
doc ─────┘ ┴ ┴ ┴ ┴ └─
txt ─────┘ ┴ ┴ ┴ ┴ └─
par ─────┘ ┴ ┴ ┴ ┴ └─
pid ─────┘ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────────────────────────────────────
492 measurable_const
src ─────┘ └
typ ─────┘ └
doc ─────┘ └
txt ─────┘ └
par ─────┘ └
pid ─────┘ └
st ───────────────────────
493 measurable_const }
id └──────────────┘
src ─────┘└──────────────┘┴
typ ─────┘└──────────────┘┴
doc ─────┘ ┴
txt ─────┘ ┴
par ─────┘ ┴
pid ─────┘ ┴
st ──────────────────────┘└─
494 end
st ──┘
495
496 lemma measurable.add {α : Type*} [measurable_space α] {f g : α → ennreal} :
id └──────────────┘ ┴ ┴ └─────┘
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ ┴ └─────┘
doc └─────┘
497 measurable f → measurable g → measurable (λa, f a + g a) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
498 begin
st └─────
499 refine measurable_of_measurable_nnreal_nnreal (+) _ _ _,
id └────────────────────────────────────┘ ┴
src └─────┘└────────────────────────────────────┘┴┴└──────┘
typ └─────┘└────────────────────────────────────┘┴┴└──────┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ────────────────────────────────────────────────────────┘└─
500 { simp only [ennreal.coe_add.symm],
src └─────────┘ ┴
typ └─────────┘└──────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───┘└──────────────────────────────┘└─
501 exact measurable_coe.comp
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ──────────────────────────────
502 (measurable.add (measurable.fst measurable_id) (measurable.snd measurable_id)) },
id └────────────┘ └────────────┘ └────────────┘ └───────────┘
src ─────┘ └────────────┘┴ └────────────┘┴ └┘ └────────────┘┴└───────────┘└─┘
typ ─────┘ └────────────┘┴ └────────────┘┴ └┘ └────────────┘┴└───────────┘└─┘
doc ─────┘ ┴ ┴ └┘ ┴ └─┘
txt ─────┘ ┴ ┴ └┘ ┴ └─┘
par ─────┘ ┴ ┴ └┘ ┴ └─┘
pid ─────┘ ┴ ┴ └┘ ┴ └┘┴
st ────────────────────────────────────────────────────────────────────────────────────┘└┘└
503 { simp [measurable_const] },
id └──────────────┘
src └────┘└──────────────┘└┘
typ └────┘└──────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└──────────────────────┘└┘└
504 { simp [measurable_const] }
id └──────────────┘
src └────┘└──────────────┘└┘
typ └────┘└──────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───────────────────────────┘└─
505 end
st ──┘
506
507 lemma measurable.sub {α : Type*} [measurable_space α] {f g : α → ennreal} :
id └──────────────┘ ┴ ┴ └─────┘
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ ┴ └─────┘
doc └─────┘
508 measurable f → measurable g → measurable (λa, f a - g a) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
509 begin
st └─────
510 refine measurable_of_measurable_nnreal_nnreal (has_sub.sub) _ _ _,
id └────────────────────────────────────┘ └─────────┘
src └─────┘└────────────────────────────────────┘┴ └─────────┘└─────┘
typ └─────┘└────────────────────────────────────┘┴ └─────────┘└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ──────────────────────────────────────────────────────────────────┘└─
511 { simp only [ennreal.coe_sub.symm],
src └─────────┘ ┴
typ └─────────┘└──────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───┘└──────────────────────────────┘└─
512 exact measurable_coe.comp
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ──────────────────────────────
513 (nnreal.measurable.sub (measurable.fst measurable_id) (measurable.snd measurable_id)) },
id └───────────────────┘ └────────────┘ └────────────┘ └───────────┘
src ─────┘ └───────────────────┘┴ └────────────┘┴ └┘ └────────────┘┴└───────────┘└─┘
typ ─────┘ └───────────────────┘┴ └────────────┘┴ └┘ └────────────┘┴└───────────┘└─┘
doc ─────┘ ┴ ┴ └┘ ┴ └─┘
txt ─────┘ ┴ ┴ └┘ ┴ └─┘
par ─────┘ ┴ ┴ └┘ ┴ └─┘
pid ─────┘ ┴ ┴ └┘ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘└┘└
514 { simp [measurable_const] },
id └──────────────┘
src └────┘└──────────────┘└┘
typ └────┘└──────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└──────────────────────┘└┘└
515 { simp [measurable_const] }
id └──────────────┘
src └────┘└──────────────┘└┘
typ └────┘└──────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───────────────────────────┘└─
516 end
st ──┘
517
518 lemma measurable_of_real : measurable ennreal.of_real :=
id └────────┘ └─────────────┘
src └────────┘ └─────────────┘
typ └────────┘ └─────────────┘
doc └────────┘ └─────────────┘
519 measurable_of_continuous ennreal.continuous_of_real
id └──────────────────────┘ └────────────────────────┘
src └──────────────────────┘ └────────────────────────┘
typ └──────────────────────┘ └────────────────────────┘
520
521 end ennreal
522
523 open topological_space
524
525 lemma measurable.smul' {α : Type*} {β : Type*} {γ : Type*}
526 [semiring α] [topological_space α] [second_countable_topology α]
id └──────┘ ┴ └───────────────┘ ┴ └───────────────────────┘ ┴
src └──────┘ └───────────────┘ └───────────────────────┘
typ └──────┘ ┴ └───────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────────┘
527 [topological_space β] [add_comm_monoid β] [second_countable_topology β]
id └───────────────┘ ┴ └─────────────┘ ┴ └───────────────────────┘ ┴
src └───────────────┘ └─────────────┘ └───────────────────────┘
typ └───────────────┘ ┴ └─────────────┘ ┴ └───────────────────────┘ ┴
doc └───────────────┘ └───────────────────────┘
528 [semimodule α β] [topological_semimodule α β] [measurable_space γ]
id └────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └──────────────┘ ┴
src └────────┘ └────────────────────┘ └──────────────┘
typ └────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └──────────────┘ ┴
doc └────────┘ └────────────────────┘
529 {f : γ → α} {g : γ → β} (hf : measurable f) (hg : measurable g) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
530 measurable (λ c, f c • g c) :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
531 measurable_of_continuous2 (continuous_fst.smul continuous_snd) hf hg
id └───────────────────────┘ └────────────┘└───┘ └────────────┘ └┘ └┘
src └───────────────────────┘ └────────────┘└───┘ └────────────┘
typ └───────────────────────┘ └────────────┘└───┘ └────────────┘ └┘ └┘
532
533 lemma measurable.smul {α : Type*} {β : Type*} {γ : Type*}
534 [semiring α] [topological_space α]
id └──────┘ ┴ └───────────────┘ ┴
src └──────┘ └───────────────┘
typ └──────┘ ┴ └───────────────┘ ┴
doc └───────────────┘
535 [topological_space β] [add_comm_monoid β]
id └───────────────┘ ┴ └─────────────┘ ┴
src └───────────────┘ └─────────────┘
typ └───────────────┘ ┴ └─────────────┘ ┴
doc └───────────────┘
536 [semimodule α β] [topological_semimodule α β] [measurable_space γ]
id └────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └──────────────┘ ┴
src └────────┘ └────────────────────┘ └──────────────┘
typ └────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └──────────────┘ ┴
doc └────────┘ └────────────────────┘
537 (c : α) {f : γ → β} (hf : measurable f) : measurable (λ x, c • f x) :=
id ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
538 measurable.comp (measurable_of_continuous (continuous_const.smul continuous_id)) hf
id └─────────────┘ └──────────────────────┘ └──────────────┘└───┘ └───────────┘ └┘
src └─────────────┘ └──────────────────────┘ └──────────────┘└───┘ └───────────┘
typ └─────────────┘ └──────────────────────┘ └──────────────┘└───┘ └───────────┘ └┘
539
540 lemma measurable_smul_iff {α : Type*} {β : Type*} {γ : Type*}
541 [division_ring α] [topological_space α]
id └───────────┘ ┴ └───────────────┘ ┴
src └───────────┘ └───────────────┘
typ └───────────┘ ┴ └───────────────┘ ┴
doc └───────────────┘
542 [topological_space β] [add_comm_monoid β]
id └───────────────┘ ┴ └─────────────┘ ┴
src └───────────────┘ └─────────────┘
typ └───────────────┘ ┴ └─────────────┘ ┴
doc └───────────────┘
543 [semimodule α β] [topological_semimodule α β] [measurable_space γ]
id └────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └──────────────┘ ┴
src └────────┘ └────────────────────┘ └──────────────┘
typ └────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └──────────────┘ ┴
doc └────────┘ └────────────────────┘
544 {c : α} (hc : c ≠ 0) (f : γ → β) : measurable (λ x, c • f x) ↔ measurable f :=
id ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
src ┴ └────────┘ ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
545 iff.intro
id └───────┘
src └───────┘
typ └───────┘
546 begin
st └─────
547 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
548 have eq : (λ (x : γ), c⁻¹ • (λ (x : γ), c • f x) x) = f,
id └┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────┘ └─┘ └┘┴┴┴ └────┘ └─┘ ┴ ┴ ┴ └┘ └┘┴┴
typ └────────┘ └────┘ └─┘ └┘┴┴┴ └────┘┴└─┘┴┴ ┴ ┴ └┘ └┘┴┴┴
doc └────────┘ └────┘ └─┘ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ └┘ ┴
txt └────────┘ └────┘ └─┘ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ └┘ ┴
par └────────┘ └────┘ └─┘ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ └┘ ┴
pid └─────┘└─┘ └────┘ └─┘ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ └┘ ┴
st ────────────────────────────────────────────────────────┘└─
549 { funext, rw [smul_smul, inv_mul_cancel hc, one_smul] },
id └───────┘ └────────────┘ └┘ └──────┘
src └────┘ └──┘└───────┘└┘└────────────┘┴ └┘└──────┘└┘
typ └────┘ └──┘└───────┘└┘└────────────┘┴└┘└┘└──────┘└┘
doc └────┘ └──┘ └┘ ┴ └┘ └┘
txt └────┘ └──┘ └┘ ┴ └┘ └┘
par └────┘ └──┘ └┘ ┴ └┘ └┘
pid └┘ └┘ ┴ └┘ ┴┴
st ───┘└────┘└─────────────┘└─────────────────┘└────────┘┴┴└┘└
550 have := h.smul c⁻¹,
id └────┘ ┴
src └──────┘└────┘┴
typ └──────┘└────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ───────────────────┘└─
551 rwa eq at this
id └┘
src └──┘└┘└───────┘
typ └──┘└┘└───────┘
doc └──┘ └───────┘
txt └──┘ └───────┘
par └──┘ └───────┘
pid ┴ └──────┘┴
st ────────────────┘
552 end
st └─┘
553 $ measurable.smul c
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
554
555 lemma measurable_dist {α : Type*} [metric_space α] [second_countable_topology α] :
id └──────────┘ ┴ └───────────────────────┘ ┴
src └──────────┘ └───────────────────────┘
typ └──────────┘ ┴ └───────────────────────┘ ┴
doc └──────────┘ └───────────────────────┘
556 measurable (λp:α×α, dist p.1 p.2) :=
id └────────┘ ┴┴┴ └──┘ ┴┴ ┴┴
src └────────┘ ┴ └──┘ ┴ ┴
typ └────────┘ ┴┴┴ └──┘ ┴┴ ┴┴
doc └────────┘
557 begin
st └─────
558 rw [borel_prod],
id └────────┘
src └──┘└────────┘┴
typ └──┘└────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────┘└──
559 apply measurable_of_continuous,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────┘└─
560 exact continuous_dist continuous_fst continuous_snd
id └─────────────┘ └────────────┘ └────────────┘
src └────┘└─────────────┘┴└────────────┘┴└────────────┘┴
typ └────┘└─────────────┘┴└────────────┘┴└────────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────┘
561 end
st └─┘
562
563 lemma measurable.dist {α : Type*} [metric_space α] [second_countable_topology α]
id └──────────┘ ┴ └───────────────────────┘ ┴
src └──────────┘ └───────────────────────┘
typ └──────────┘ ┴ └───────────────────────┘ ┴
doc └──────────┘ └───────────────────────┘
564 [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └──────────────┘ └────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
565 measurable (λ b, dist (f b) (g b)) :=
id └────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
src └────────┘ └──┘
typ └────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
doc └────────┘
566 measurable_dist.comp (measurable.prod_mk hf hg)
id └─────────────┘└───┘ └────────────────┘ └┘ └┘
src └─────────────┘└───┘ └────────────────┘
typ └─────────────┘└───┘ └────────────────┘ └┘ └┘
567
568 lemma measurable_nndist {α : Type*} [metric_space α] [second_countable_topology α] :
id └──────────┘ ┴ └───────────────────────┘ ┴
src └──────────┘ └───────────────────────┘
typ └──────────┘ ┴ └───────────────────────┘ ┴
doc └──────────┘ └───────────────────────┘
569 measurable (λp:α×α, nndist p.1 p.2) :=
id └────────┘ ┴┴┴ └────┘ ┴┴ ┴┴
src └────────┘ ┴ └────┘ ┴ ┴
typ └────────┘ ┴┴┴ └────┘ ┴┴ ┴┴
doc └────────┘ └────┘
570 begin
st └─────
571 rw [borel_prod],
id └────────┘
src └──┘└────────┘┴
typ └──┘└────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────┘└──
572 apply measurable_of_continuous,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────┘└─
573 exact continuous_nndist continuous_fst continuous_snd
id └───────────────┘ └────────────┘ └────────────┘
src └────┘└───────────────┘┴└────────────┘┴└────────────┘┴
typ └────┘└───────────────┘┴└────────────┘┴└────────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘
574 end
st └─┘
575
576 lemma measurable.nndist {α : Type*} [metric_space α] [second_countable_topology α]
id └──────────┘ ┴ └───────────────────────┘ ┴
src └──────────┘ └───────────────────────┘
typ └──────────┘ ┴ └───────────────────────┘ ┴
doc └──────────┘ └───────────────────────┘
577 [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └──────────────┘ └────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
578 measurable (λ b, nndist (f b) (g b)) :=
id └────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └────────┘ └────┘
typ └────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────┘
579 measurable_nndist.comp (measurable.prod_mk hf hg)
id └───────────────┘└───┘ └────────────────┘ └┘ └┘
src └───────────────┘└───┘ └────────────────┘
typ └───────────────┘└───┘ └────────────────┘ └┘ └┘
580
581 lemma measurable_edist {α : Type*} [emetric_space α] [second_countable_topology α] :
id └───────────┘ ┴ └───────────────────────┘ ┴
src └───────────┘ └───────────────────────┘
typ └───────────┘ ┴ └───────────────────────┘ ┴
doc └───────────┘ └───────────────────────┘
582 measurable (λp:α×α, edist p.1 p.2) :=
id └────────┘ ┴┴┴ └───┘ ┴┴ ┴┴
src └────────┘ ┴ └───┘ ┴ ┴
typ └────────┘ ┴┴┴ └───┘ ┴┴ ┴┴
doc └────────┘
583 begin
st └─────
584 rw [borel_prod],
id └────────┘
src └──┘└────────┘┴
typ └──┘└────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────┘└──
585 apply measurable_of_continuous,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────┘└─
586 exact continuous_edist continuous_fst continuous_snd
id └──────────────┘ └────────────┘ └────────────┘
src └────┘└──────────────┘┴└────────────┘┴└────────────┘┴
typ └────┘└──────────────┘┴└────────────┘┴└────────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────┘
587 end
st └─┘
588
589 lemma measurable.edist {α : Type*} [emetric_space α] [second_countable_topology α]
id └───────────┘ ┴ └───────────────────────┘ ┴
src └───────────┘ └───────────────────────┘
typ └───────────┘ ┴ └───────────────────────┘ ┴
doc └───────────┘ └───────────────────────┘
590 [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └──────────────┘ └────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
591 measurable (λ b, edist (f b) (g b)) :=
id └────────┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └────────┘ └───┘
typ └────────┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └────────┘
592 measurable_edist.comp (measurable.prod_mk hf hg)
id └──────────────┘└───┘ └────────────────┘ └┘ └┘
src └──────────────┘└───┘ └────────────────┘
typ └──────────────┘└───┘ └────────────────┘ └┘ └┘
593
594 lemma measurable_norm {α : Type*} [normed_group α] : measurable (norm : α → ℝ) :=
id └──────────┘ ┴ └────────┘ └──┘ ┴ ┴
src └──────────┘ └────────┘ └──┘ ┴
typ └──────────┘ ┴ └────────┘ └──┘ ┴ ┴
doc └──────────┘ └────────┘
595 measurable_of_continuous continuous_norm
id └──────────────────────┘ └─────────────┘
src └──────────────────────┘ └─────────────┘
typ └──────────────────────┘ └─────────────┘
596
597 lemma measurable.norm {α : Type*} [normed_group α] [measurable_space β]
id └──────────┘ ┴ └──────────────┘ ┴
src └──────────┘ └──────────────┘
typ └──────────┘ ┴ └──────────────┘ ┴
doc └──────────┘
598 {f : β → α} (hf : measurable f) : measurable (λa, norm (f a)) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ └──┘ ┴ ┴
src └────────┘ └────────┘ └──┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └──┘ ┴ ┴
doc └────────┘ └────────┘
599 measurable_norm.comp hf
id └─────────────┘└───┘ └┘
src └─────────────┘└───┘
typ └─────────────┘└───┘ └┘
600
601 lemma measurable_nnnorm {α : Type*} [normed_group α] : measurable (nnnorm : α → nnreal) :=
id └──────────┘ ┴ └────────┘ └────┘ ┴ └────┘
src └──────────┘ └────────┘ └────┘ └────┘
typ └──────────┘ ┴ └────────┘ └────┘ ┴ └────┘
doc └──────────┘ └────────┘ └────┘ └────┘
602 measurable_of_continuous continuous_nnnorm
id └──────────────────────┘ └───────────────┘
src └──────────────────────┘ └───────────────┘
typ └──────────────────────┘ └───────────────┘
603
604 lemma measurable.nnnorm {α : Type*} [normed_group α] [measurable_space β]
id └──────────┘ ┴ └──────────────┘ ┴
src └──────────┘ └──────────────┘
typ └──────────┘ ┴ └──────────────┘ ┴
doc └──────────┘
605 {f : β → α} (hf : measurable f) : measurable (λa, nnnorm (f a)) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────┘ ┴ ┴
src └────────┘ └────────┘ └────┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────┘ ┴ ┴
doc └────────┘ └────────┘ └────┘
606 measurable_nnnorm.comp hf
id └───────────────┘└───┘ └┘
src └───────────────┘└───┘
typ └───────────────┘└───┘ └┘
607
608 lemma measurable.coe_nnnorm {α : Type*} [normed_group α] [measurable_space β]
id └──────────┘ ┴ └──────────────┘ ┴
src └──────────┘ └──────────────┘
typ └──────────┘ ┴ └──────────────┘ ┴
doc └──────────┘
609 {f : β → α} (hf : measurable f) : measurable (λa, (nnnorm (f a) : ennreal)) :=
id ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────┘ ┴ ┴ └─────┘
src └────────┘ └────────┘ └────┘ └─────┘
typ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────┘ ┴ ┴ └─────┘
doc └────────┘ └────────┘ └────┘ └─────┘
610 ennreal.measurable_coe.comp $ hf.nnnorm
id └────────────────────┘└───┘ └┘└─────┘
src └────────────────────┘└───┘ └─────┘
typ └────────────────────┘└───┘ └┘└─────┘